let G be addGroup; :: thesis: ( G is Abelian addGroup implies for H being strict Subgroup of G
for a being Element of G holds H * a = H )
assume A1: G is Abelian addGroup ; :: thesis: for H being strict Subgroup of G
for a being Element of G holds H * a = H
let H be strict Subgroup of G; :: thesis: for a being Element of G holds H * a = H
let a be Element of G; :: thesis: H * a = H
the carrier of (H * a) = ((- a) + H) + a by ThB59
.= (H + (- a)) + a by A1, Th112
.= H + ((- a) + a) by ThA107
.= H + (0_ G) by Def5
.= the carrier of H by ThB109 ;
hence H * a = H by Th59; :: thesis: verum