now :: thesis: for H being strict Subgroup of G st H = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) holds

H is normal

hence
(1). G is normal
; :: thesis: verumH is normal

reconsider G9 = G as Group ;

let H be strict Subgroup of G; :: thesis: ( H = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) implies H is normal )

reconsider H9 = H as strict Subgroup of G9 ;

assume H = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) ; :: thesis: H is normal

then the carrier of H = {(1_ G)} by Def8;

then H9 = (1). G9 by GROUP_2:def 7;

hence H is normal ; :: thesis: verum

end;let H be strict Subgroup of G; :: thesis: ( H = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) implies H is normal )

reconsider H9 = H as strict Subgroup of G9 ;

assume H = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) ; :: thesis: H is normal

then the carrier of H = {(1_ G)} by Def8;

then H9 = (1). G9 by GROUP_2:def 7;

hence H is normal ; :: thesis: verum