let G be non empty multMagma ; :: thesis: for A, B being Subset of G st ( for a, b being Element of G st a in A & b in B holds

a * b = b * a ) holds

A * B = B * A

let A, B be Subset of G; :: thesis: ( ( for a, b being Element of G st a in A & b in B holds

a * b = b * a ) implies A * B = B * A )

assume A1: for a, b being Element of G st a in A & b in B holds

a * b = b * a ; :: thesis: A * B = B * A

thus A * B c= B * A :: according to XBOOLE_0:def 10 :: thesis: B * A c= A * B

assume x in B * A ; :: thesis: x in A * B

then consider b, a being Element of G such that

A4: x = b * a and

A5: ( b in B & a in A ) ;

x = a * b by A1, A4, A5;

hence x in A * B by A5; :: thesis: verum

a * b = b * a ) holds

A * B = B * A

let A, B be Subset of G; :: thesis: ( ( for a, b being Element of G st a in A & b in B holds

a * b = b * a ) implies A * B = B * A )

assume A1: for a, b being Element of G st a in A & b in B holds

a * b = b * a ; :: thesis: A * B = B * A

thus A * B c= B * A :: according to XBOOLE_0:def 10 :: thesis: B * A c= A * B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B * A or x in A * B )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A * B or x in B * A )

assume x in A * B ; :: thesis: x in B * A

then consider a, b being Element of G such that

A2: x = a * b and

A3: ( a in A & b in B ) ;

x = b * a by A1, A2, A3;

hence x in B * A by A3; :: thesis: verum

end;assume x in A * B ; :: thesis: x in B * A

then consider a, b being Element of G such that

A2: x = a * b and

A3: ( a in A & b in B ) ;

x = b * a by A1, A2, A3;

hence x in B * A by A3; :: thesis: verum

assume x in B * A ; :: thesis: x in A * B

then consider b, a being Element of G such that

A4: x = b * a and

A5: ( b in B & a in A ) ;

x = a * b by A1, A4, A5;

hence x in A * B by A5; :: thesis: verum