let O be set ; :: thesis: for G being GroupWithOperators of O holds nat_hom ((1). G) is bijective

let G be GroupWithOperators of O; :: thesis: 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; :: thesis: verum

let G be GroupWithOperators of O; :: thesis: 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; :: thesis: verum