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

proof

assume A1: H is normal Subgroup of G ; :: thesis: for a being Element of G holds H * a is Subgroup of H
let a be Element of G; :: thesis: H * a is Subgroup of H
H * a = addMagma(# the carrier of H, the addF of H #) by A1, Def13;
hence H * a is Subgroup of H by ThA54; :: thesis: verum

end;

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

now :: thesis: for a being Element of G holds a + H c= H + a

let a be Element of G; :: thesis: a + H c= H + a
A3: (H * (- a)) + a = (((- (- a)) + H) + (- a)) + a by ThB59
.= ((- (- a)) + H) + ((- a) + a) by ThB34
.= ((- (- a)) + H) + (0_ G) by Def5
.= a + H by Th37 ;
H * (- a) is Subgroup of H by A2;
hence a + H c= H + a by A3, ThB6; :: thesis: verum

end;

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