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
set g = nat_hom ((1). G);
reconsider G' = G as Group ;
reconsider H = multMagma(# the carrier of ((1). G),the multF of ((1). G) #) as strict normal Subgroup of G by Lm7;
A1: the carrier of H = {(1_ G')} by Def8;
A2: nat_hom ((1). G) = nat_hom H by Def23
.= nat_hom ((1). G') by A1, GROUP_2:def 7 ;
nat_hom ((1). G') is bijective by GROUP_6:75;
then nat_hom ((1). G') is one-to-one ;
then nat_hom ((1). G) is one-to-one by A2;
then ( nat_hom ((1). G) is one-to-one & nat_hom ((1). G) is onto ) by Th53;
hence nat_hom ((1). G) is bijective ; :: thesis: verum