let F be Field; :: thesis: canHom_Int F = (canHom_Rat F) | INT
set f = canHom_Int F;
set g = canHom_Rat F;
dom (canHom_Rat F) = RAT by FUNCT_2:def 1;
then A1: dom ((canHom_Rat F) | INT) = INT by RELAT_1:62, NUMBERS:14;
now :: thesis: for x being object st x in dom (canHom_Int F) holds
(canHom_Int F) . x = ((canHom_Rat F) | INT) . x
let x be object ; :: thesis: ( x in dom (canHom_Int F) implies (canHom_Int F) . x = ((canHom_Rat F) | INT) . x )
assume A2: x in dom (canHom_Int F) ; :: thesis: (canHom_Int F) . x = ((canHom_Rat F) | INT) . x
then reconsider y = x as Element of INT.Ring ;
reconsider r = y as Element of F_Rat by NUMBERS:14;
A3: (canHom_Int F) . (1_ INT.Ring) = 1_ F by GROUP_1:def 13;
thus (canHom_Int F) . x = ((canHom_Int F) . (numerator r)) / (1_ F) by RAT_1:17
.= ((canHom_Int F) . (numerator r)) / ((canHom_Int F) . (denominator r)) by A3, RAT_1:17
.= (canHom_Rat F) . x by Def11
.= ((canHom_Rat F) | INT) . x by A2, FUNCT_1:49 ; :: thesis: verum
end;
hence canHom_Int F = (canHom_Rat F) | INT by FUNCT_2:def 1, A1; :: thesis: verum