let G be Group; :: thesis: ( G is commutative Group iff for A being Subset of G
for g being Element of G st A <> {} holds
g |^ A = {g} )
thus ( G is commutative Group 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 commutative Group )
assume A1: for A being Subset of G
for g being Element of G st A <> {} holds
g |^ A = {g} ; :: thesis: G is commutative Group

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 Th37 ;
hence a = a |^ b by ZFMISC_1:3; :: thesis: verum

end;

hence G is commutative Group by Th30; :: thesis: verum