let G be addGroup; :: thesis: ( G is Abelian addGroup iff for A being Subset of G
for g being Element of G st A <> {} holds
g * A = {g} )
thus ( G is Abelian addGroup implies for A being Subset of G
for g being Element of G st A <> {} holds
g * A = {g} ) by Th55; :: thesis: ( ( for A being Subset of G
for g being Element of G st A <> {} holds
g * A = {g} ) implies G is Abelian addGroup )
assume A1: for A being Subset of G
for g being Element of G st A <> {} holds
g * A = {g} ; :: 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