let G be addGroup; :: 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 Th117; :: 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
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
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 ThB105;
then a + (H + (- a)) c= (0_ G) + H by Def5;
then a + (H + (- a)) c= carr H by ThB109;
then (a + H) + (- a) c= carr H by ThB106;
then ((a + H) + (- a)) + a c= (carr H) + a by Th4;
then (a + H) + ((- a) + a) c= H + a by ThB34;
then (a + H) + (0_ G) c= H + a by Def5;
hence a + H c= H + a by Th37; :: 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