now

reconsider G9 = G as Group ;
let H be strict Subgroup of G; :: thesis: ( H = multMagma(# the carrier of ((Omega). G), the multF of ((Omega). G) #) implies H is normal )
reconsider H9 = H as strict Subgroup of G9 ;
assume H = multMagma(# the carrier of ((Omega). G), the multF of ((Omega). G) #) ; :: thesis: H is normal
then H9 = (Omega). G9 ;
hence H is normal ; :: thesis: verum

end;

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