let G be Group; :: thesis: for H being Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds a * H = H * a )
let H be Subgroup of G; :: thesis: ( H is normal Subgroup of G iff for a being Element of G holds a * H = H * a )
thus ( H is normal Subgroup of G implies for a being Element of G holds a * H = H * a ) :: thesis: ( ( for a being Element of G holds a * H = H * a ) implies H is normal Subgroup of G )

proof

assume A1: H is normal Subgroup of G ; :: thesis: for a being Element of G holds a * H = H * a
let a be Element of G; :: thesis: a * H = H * a
A2: carr (H |^ a) = ((a ") * H) * a by Th59;
carr (H |^ a) = the carrier of multMagma(# the carrier of H, the multF of H #) by A1, Def13
.= carr H ;
hence a * H = (a * ((a ") * H)) * a by A2, GROUP_2:33
.= ((a * (a ")) * H) * a by GROUP_2:105
.= ((1_ G) * H) * a by GROUP_1:def 5
.= H * a by GROUP_2:37 ;
:: thesis: verum

end;

assume A3: for a being Element of G holds a * H = H * a ; :: thesis: H is normal Subgroup of G
H is normal

proof

let a be Element of G; :: according to GROUP_3:def 13 :: thesis: H |^ a = multMagma(# the carrier of H, the multF of H #)
the carrier of (H |^ a) = ((a ") * H) * a by Th59
.= (H * (a ")) * a by A3
.= H * ((a ") * a) by GROUP_2:107
.= H * (1_ G) by GROUP_1:def 5
.= the carrier of H by GROUP_2:109 ;
hence H |^ a = multMagma(# the carrier of H, the multF of H #) by GROUP_2:59; :: thesis: verum

end;

hence H is normal Subgroup of G ; :: thesis: verum