let G be Group; :: thesis: for H being Subgroup of G holds
( H is normal Subgroup of G iff for A being Subset of G holds A * H = H * A )
let H be Subgroup of G; :: thesis: ( H is normal Subgroup of G iff for A being Subset of G holds A * H = H * A )
thus ( H is normal Subgroup of G implies for A being Subset of G holds A * H = H * A ) :: thesis: ( ( for A being Subset 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 Subset of G holds A * H = H * A
let A be Subset of G; :: thesis: A * H = H * A
thus A * H c= H * A :: according to XBOOLE_0:def 10 :: thesis: H * A c= A * H

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A * H or x in H * A )
assume x in A * H ; :: thesis: x in H * A
then consider a, h being Element of G such that
A2: x = a * h and
A3: a in A and
A4: h in H by GROUP_2:94;
x in a * H by A2, A4, GROUP_2:103;
then x in H * a by A1, Th117;
then ex g being Element of G st
( x = g * a & g in H ) by GROUP_2:104;
hence x in H * A by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H * A or x in A * H )
assume x in H * A ; :: thesis: x in A * H
then consider h, a being Element of G such that
A5: ( x = h * a & h in H ) and
A6: a in A by GROUP_2:95;
x in H * a by A5, GROUP_2:104;
then x in a * H by A1, Th117;
then ex g being Element of G st
( x = a * g & g in H ) by GROUP_2:103;
hence x in A * H by A6; :: thesis: verum

end;

assume A7: for A being Subset of G holds A * H = H * A ; :: thesis: H is normal Subgroup of G

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

let a be Element of G; :: thesis: a * H = H * a
thus a * H = {a} * H
.= H * {a} by A7
.= H * a ; :: thesis: verum

end;

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