let O be set ; for G being GroupWithOperators of O holds nat_hom ((1). G) is bijective
let G be GroupWithOperators of O; nat_hom ((1). G) is bijective
reconsider H = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) as strict normal Subgroup of G by Lm6;
set g = nat_hom ((1). G);
reconsider G9 = G as Group ;
A1:
the carrier of H = {(1_ G9)}
by Def8;
A2:
( nat_hom ((1). G9) is bijective & nat_hom ((1). G) is onto )
by Th53, GROUP_6:65;
nat_hom ((1). G) =
nat_hom H
by Def20
.=
nat_hom ((1). G9)
by A1, GROUP_2:def 7
;
hence
nat_hom ((1). G) is bijective
by A2; verum