let G be addGroup; :: thesis: ( G is Abelian addGroup iff for A being Subset of G
for g being Element of G holds A * g = A )
thus ( G is Abelian addGroup implies for A being Subset of G
for g being Element of G holds A * g = A ) by Th55; :: thesis: ( ( for A being Subset of G
for g being Element of G holds A * g = A ) implies G is Abelian addGroup )
assume A1: for A being Subset of G
for g being Element of G holds A * g = A ; :: thesis: G is Abelian addGroup

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

let a, b be Element of G; :: thesis: a = a * b
{a} = {a} * b by A1
.= {(a * b)} by ThB37 ;
hence a = a * b by ZFMISC_1:3; :: thesis: verum

end;

hence G is Abelian addGroup by ThB30; :: thesis: verum