let G, H be Group; for h being Homomorphism of G,H holds
( h .: ((1). G) = (1). H & h .: ((Omega). G) = (Omega). (Image h) )
let h be Homomorphism of G,H; ( h .: ((1). G) = (1). H & h .: ((Omega). G) = (Omega). (Image h) )
A1:
dom h = the carrier of G
by FUNCT_2:def 1;
A2:
the carrier of ((1). H) = {(1_ H)}
by GROUP_2:def 7;
the carrier of ((1). G) = {(1_ G)}
by GROUP_2:def 7;
then the carrier of (h .: ((1). G)) =
Im (h,(1_ G))
by Th8
.=
{(h . (1_ G))}
by A1, FUNCT_1:59
.=
the carrier of ((1). H)
by A2, GROUP_6:31
;
hence
h .: ((1). G) = (1). H
by GROUP_2:59; h .: ((Omega). G) = (Omega). (Image h)
the carrier of (h .: ((Omega). G)) =
h .: the carrier of G
by Th8
.=
the carrier of ((Omega). (Image h))
by GROUP_6:def 10
;
hence
h .: ((Omega). G) = (Omega). (Image h)
by GROUP_2:59; verum