set f = canHom_Z/ (p,F);
set c = canHom_Int F;
1_ (Z/ p) = 1_ INT.Ring by INT_3:14, INT_2:def 4;
hence (canHom_Z/ (p,F)) . (1_ (Z/ p)) = (canHom_Int F) . (1_ INT.Ring) by FUNCT_1:49
.= 1_ F by GROUP_1:def 13 ;
:: according to GROUP_1:def 13 :: thesis: verum