now

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 G' = G as Group ;
reconsider H' = H as strict Subgroup of G' ;
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 H' = (1). G' by GROUP_2:def 7;
hence H is normal ; :: thesis: verum

end;

hence (1). G is normal by Def10; :: thesis: verum