let G be Group; :: 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 = multMagma(# the carrier of H, the multF of H #) by A1, Def13;
hence H |^ a is Subgroup of H by GROUP_2:54; :: 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 Th59
.= (((a ") ") * H) * ((a ") * a) by GROUP_2:34
.= (((a ") ") * H) * (1_ G) by GROUP_1:def 5
.= ((a ") ") * H by GROUP_2:37
.= a * H ;
H |^ (a ") is Subgroup of H by A2;
hence a * H c= H * a by A3, Th6; :: thesis: verum

end;

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