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

A2: now

let a be Element of G; :: thesis: a * H c= H * a
H * (a " ) c= (a " ) * H by A1;
then a * (H * (a " )) c= a * ((a " ) * H) by Th4;
then a * (H * (a " )) c= (a * (a " )) * H by GROUP_2:127;
then a * (H * (a " )) c= (1_ G) * H by GROUP_1:def 6;
then a * (H * (a " )) c= carr H by GROUP_2:132;
then (a * H) * (a " ) c= carr H by GROUP_2:128;
then ((a * H) * (a " )) * a c= (carr H) * a by Th4;
then (a * H) * ((a " ) * a) c= H * a by GROUP_2:40;
then (a * H) * (1_ G) c= H * a by GROUP_1:def 6;
hence a * H c= H * a by GROUP_2:43; :: thesis: verum

end;

now

let a be Element of G; :: thesis: a * H = H * a
( a * H c= H * a & H * a c= a * H ) by A1, A2;
hence a * H = H * a by XBOOLE_0:def 10; :: thesis: verum

end;

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