set f = (canHom_Int F) | the carrier of (Z/ p);
now :: thesis: for x being object st x in the carrier of (Z/ p) holds
x in dom (canHom_Int F)
let x be object ; :: thesis: ( x in the carrier of (Z/ p) implies x in dom (canHom_Int F) )
assume x in the carrier of (Z/ p) ; :: thesis: x in dom (canHom_Int F)
then reconsider x1 = x as natural Number ;
x1 in INT by NUMBERS:17, ORDINAL1:def 12;
hence x in dom (canHom_Int F) by FUNCT_2:def 1; :: thesis: verum
end;
then the carrier of (Z/ p) c= dom (canHom_Int F) ;
then A1: dom ((canHom_Int F) | the carrier of (Z/ p)) = the carrier of (Z/ p) by RELAT_1:62;
now :: thesis: for x being object st x in the carrier of (Z/ p) holds
((canHom_Int F) | the carrier of (Z/ p)) . x in the carrier of F
let x be object ; :: thesis: ( x in the carrier of (Z/ p) implies ((canHom_Int F) | the carrier of (Z/ p)) . x in the carrier of F )
assume A2: x in the carrier of (Z/ p) ; :: thesis: ((canHom_Int F) | the carrier of (Z/ p)) . x in the carrier of F
then ((canHom_Int F) | the carrier of (Z/ p)) . x = (canHom_Int F) . x by FUNCT_1:49;
then ((canHom_Int F) | the carrier of (Z/ p)) . x in rng (canHom_Int F) by A1, A2, FUNCT_2:4;
hence ((canHom_Int F) | the carrier of (Z/ p)) . x in the carrier of F ; :: thesis: verum
end;
hence (canHom_Int F) | the carrier of (Z/ p) is Function of (Z/ p),F by A1, FUNCT_2:3; :: thesis: verum