let G be Group; :: thesis: ( G is commutative Group iff for A being Subset of G
for g being Element of G holds A |^ g = A )
thus ( G is commutative Group implies for A being Subset of G
for g being Element of G holds A |^ g = A ) by Th65; :: thesis: ( ( for A being Subset of G
for g being Element of G holds A |^ g = A ) implies G is commutative Group )
assume A1: for A being Subset of G
for g being Element of G holds A |^ g = A ; :: thesis: G is commutative Group

now

let a, b be Element of G; :: thesis: a = a |^ b
{a} = {a} |^ b by A1
.= {(a |^ b)} by Th44 ;
hence a = a |^ b by ZFMISC_1:6; :: thesis: verum

end;

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