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 c= 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 c= H * a )
thus ( H is normal Subgroup of G implies for a being Element of G holds a * H c= H * a ) by Th117; :: thesis: ( ( for a being Element of G holds a * H c= H * a ) implies H is normal Subgroup of G )
assume A1: for a being Element of G holds a * H c= H * a ; :: thesis: H is normal Subgroup of G

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

let a be Element of G; :: thesis: H * a c= a * H
(a ") * H c= H * (a ") by A1;
then a * ((a ") * H) c= a * (H * (a ")) by Th4;
then (a * (a ")) * H c= a * (H * (a ")) by GROUP_2:105;
then (1_ G) * H c= a * (H * (a ")) by GROUP_1:def 5;
then carr H c= a * (H * (a ")) by GROUP_2:109;
then carr H c= (a * H) * (a ") by GROUP_2:106;
then (carr H) * a c= ((a * H) * (a ")) * a by Th4;
then H * a c= (a * H) * ((a ") * a) by GROUP_2:34;
then H * a c= (a * H) * (1_ G) by GROUP_1:def 5;
hence H * a c= a * H by GROUP_2:37; :: thesis: verum

end;

then for a being Element of G holds a * H = H * a by A1;
hence H is normal Subgroup of G by Th117; :: thesis: verum