set H = (1). G;

set H9 = (1). G;

reconsider H = (1). G as StableSubgroup of G ;

take (1). G ; :: thesis: ( (1). G is strict & (1). G is normal )

set H9 = (1). G;

reconsider H = (1). G as StableSubgroup of G ;

take (1). G ; :: thesis: ( (1). G is strict & (1). G is normal )

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

H99 is normal

hence
( (1). G is strict & (1). G is normal )
; :: thesis: verumH99 is normal

reconsider G9 = G as Group ;

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

assume A1: H99 = multMagma(# the carrier of H, the multF of H #) ; :: thesis: H99 is normal

A2: the multF of ((1). G9) = the multF of G9 || the carrier of ((1). G9) by GROUP_2:def 5;

the carrier of ((1). G9) = {(1_ G9)} by GROUP_2:def 7

.= the carrier of ((1). G) by Def8 ;

hence H99 is normal by A1, A2, GROUP_2:def 5; :: thesis: verum

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

assume A1: H99 = multMagma(# the carrier of H, the multF of H #) ; :: thesis: H99 is normal

A2: the multF of ((1). G9) = the multF of G9 || the carrier of ((1). G9) by GROUP_2:def 5;

the carrier of ((1). G9) = {(1_ G9)} by GROUP_2:def 7

.= the carrier of ((1). G) by Def8 ;

hence H99 is normal by A1, A2, GROUP_2:def 5; :: thesis: verum