let X, Y be set ; :: thesis: for D being non empty set

for o being BinOp of D st o is commutative holds

o .: [:X,Y:] = o .: [:Y,X:]

let D be non empty set ; :: thesis: for o being BinOp of D st o is commutative holds

o .: [:X,Y:] = o .: [:Y,X:]

let o be BinOp of D; :: thesis: ( o is commutative implies o .: [:X,Y:] = o .: [:Y,X:] )

assume A1: for a, b being Element of D holds o . (a,b) = o . (b,a) ; :: according to BINOP_1:def 2 :: thesis: o .: [:X,Y:] = o .: [:Y,X:]

for o being BinOp of D st o is commutative holds

o .: [:X,Y:] = o .: [:Y,X:]

let D be non empty set ; :: thesis: for o being BinOp of D st o is commutative holds

o .: [:X,Y:] = o .: [:Y,X:]

let o be BinOp of D; :: thesis: ( o is commutative implies o .: [:X,Y:] = o .: [:Y,X:] )

assume A1: for a, b being Element of D holds o . (a,b) = o . (b,a) ; :: according to BINOP_1:def 2 :: thesis: o .: [:X,Y:] = o .: [:Y,X:]

now :: thesis: for X, Y being set holds o .: [:X,Y:] c= o .: [:Y,X:]

hence
( o .: [:X,Y:] c= o .: [:Y,X:] & o .: [:Y,X:] c= o .: [:X,Y:] )
; :: according to XBOOLE_0:def 10 :: thesis: verumlet X, Y be set ; :: thesis: o .: [:X,Y:] c= o .: [:Y,X:]

thus o .: [:X,Y:] c= o .: [:Y,X:] :: thesis: verum

end;thus o .: [:X,Y:] c= o .: [:Y,X:] :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in o .: [:X,Y:] or x in o .: [:Y,X:] )

assume x in o .: [:X,Y:] ; :: thesis: x in o .: [:Y,X:]

then consider y being object such that

A2: y in dom o and

A3: y in [:X,Y:] and

A4: x = o . y by FUNCT_1:def 6;

reconsider y = y as Element of [:D,D:] by A2;

y = [(y `1),(y `2)] by MCART_1:21;

then ( y `1 in X & y `2 in Y ) by A3, ZFMISC_1:87;

then A5: [(y `2),(y `1)] in [:Y,X:] by ZFMISC_1:87;

A6: ( dom o = [:D,D:] & o . ((y `1),(y `2)) = o . ((y `2),(y `1)) ) by A1, FUNCT_2:def 1;

x = o . ((y `1),(y `2)) by A4, MCART_1:21;

hence x in o .: [:Y,X:] by A6, A5, FUNCT_1:def 6; :: thesis: verum

end;assume x in o .: [:X,Y:] ; :: thesis: x in o .: [:Y,X:]

then consider y being object such that

A2: y in dom o and

A3: y in [:X,Y:] and

A4: x = o . y by FUNCT_1:def 6;

reconsider y = y as Element of [:D,D:] by A2;

y = [(y `1),(y `2)] by MCART_1:21;

then ( y `1 in X & y `2 in Y ) by A3, ZFMISC_1:87;

then A5: [(y `2),(y `1)] in [:Y,X:] by ZFMISC_1:87;

A6: ( dom o = [:D,D:] & o . ((y `1),(y `2)) = o . ((y `2),(y `1)) ) by A1, FUNCT_2:def 1;

x = o . ((y `1),(y `2)) by A4, MCART_1:21;

hence x in o .: [:Y,X:] by A6, A5, FUNCT_1:def 6; :: thesis: verum