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 a + H = 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 = H + a )
thus ( H is normal Subgroup of G implies for a being Element of G holds a + H = H + a ) :: thesis: ( ( for a being Element 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 Element of G holds a + H = H + a
let a be Element of G; :: thesis: a + H = H + a
A2: carr (H * a) = ((- a) + H) + a by ThB59;
carr (H * a) = the carrier of addMagma(# the carrier of H, the addF of H #) by A1, Def13
.= carr H ;
hence a + H = (a + ((- a) + H)) + a by A2, ThA33
.= ((a + (- a)) + H) + a by ThB105
.= ((0_ G) + H) + a by Def5
.= H + a by Th37 ;
:: thesis: verum

end;

assume A3: for a being Element of G holds a + H = H + a ; :: thesis: H is normal Subgroup of G
H is normal

proof

let a be Element of G; :: according to GROUP_1A:def 41 :: thesis: H * a = addMagma(# the carrier of H, the addF of H #)
the carrier of (H * a) = ((- a) + H) + a by ThB59
.= (H + (- a)) + a by A3
.= H + ((- a) + a) by ThA107
.= H + (0_ G) by Def5
.= the carrier of H by ThB109 ;
hence H * a = addMagma(# the carrier of H, the addF of H #) by Th59; :: thesis: verum

end;

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