let X, Y, Z be set ; :: thesis: for D being non empty set
for o being BinOp of D st o is associative holds
o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):]
let D be non empty set ; :: thesis: for o being BinOp of D st o is associative holds
o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):]
let o be BinOp of D; :: thesis: ( o is associative implies o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):] )
A1: dom o = [:D,D:] by FUNCT_2:def 1;
assume A2: for a, b, c being Element of D holds o . ((o . (a,b)),c) = o . (a,(o . (b,c))) ; :: according to BINOP_1:def 3 :: thesis: o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):]
thus o .: [:(o .: [:X,Y:]),Z:] c= o .: [:X,(o .: [:Y,Z:]):] :: according to XBOOLE_0:def 10 :: thesis: o .: [:X,(o .: [:Y,Z:]):] c= o .: [:(o .: [:X,Y:]),Z:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in o .: [:(o .: [:X,Y:]),Z:] or x in o .: [:X,(o .: [:Y,Z:]):] )
assume x in o .: [:(o .: [:X,Y:]),Z:] ; :: thesis: x in o .: [:X,(o .: [:Y,Z:]):]
then consider y being object such that
A3: y in dom o and
A4: y in [:(o .: [:X,Y:]),Z:] and
A5: x = o . y by FUNCT_1:def 6;
reconsider y = y as Element of [:D,D:] by A3;
A6: y = [(y `1),(y `2)] by MCART_1:21;
then A7: y `2 in Z by A4, ZFMISC_1:87;
y `1 in o .: [:X,Y:] by A4, A6, ZFMISC_1:87;
then consider z being object such that
A8: z in dom o and
A9: z in [:X,Y:] and
A10: y `1 = o . z by FUNCT_1:def 6;
reconsider z = z as Element of [:D,D:] by A8;
A11: y `1 = o . ((z `1),(z `2)) by A10, MCART_1:21;
A12: z = [(z `1),(z `2)] by MCART_1:21;
then z `2 in Y by A9, ZFMISC_1:87;
then [(z `2),(y `2)] in [:Y,Z:] by A7, ZFMISC_1:87;
then A13: o . ((z `2),(y `2)) in o .: [:Y,Z:] by A1, FUNCT_1:def 6;
z `1 in X by A9, A12, ZFMISC_1:87;
then A14: [(z `1),(o . ((z `2),(y `2)))] in [:X,(o .: [:Y,Z:]):] by A13, ZFMISC_1:87;
x = o . ((y `1),(y `2)) by A5, MCART_1:21;
then x = o . ((z `1),(o . ((z `2),(y `2)))) by A2, A11;
hence x in o .: [:X,(o .: [:Y,Z:]):] by A1, A14, FUNCT_1:def 6; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in o .: [:X,(o .: [:Y,Z:]):] or x in o .: [:(o .: [:X,Y:]),Z:] )
assume x in o .: [:X,(o .: [:Y,Z:]):] ; :: thesis: x in o .: [:(o .: [:X,Y:]),Z:]
then consider y being object such that
A15: y in dom o and
A16: y in [:X,(o .: [:Y,Z:]):] and
A17: x = o . y by FUNCT_1:def 6;
reconsider y = y as Element of [:D,D:] by A15;
A18: y = [(y `1),(y `2)] by MCART_1:21;
then A19: y `1 in X by A16, ZFMISC_1:87;
y `2 in o .: [:Y,Z:] by A16, A18, ZFMISC_1:87;
then consider z being object such that
A20: z in dom o and
A21: z in [:Y,Z:] and
A22: y `2 = o . z by FUNCT_1:def 6;
reconsider z = z as Element of [:D,D:] by A20;
A23: y `2 = o . ((z `1),(z `2)) by A22, MCART_1:21;
A24: z = [(z `1),(z `2)] by MCART_1:21;
then z `1 in Y by A21, ZFMISC_1:87;
then [(y `1),(z `1)] in [:X,Y:] by A19, ZFMISC_1:87;
then A25: o . ((y `1),(z `1)) in o .: [:X,Y:] by A1, FUNCT_1:def 6;
z `2 in Z by A21, A24, ZFMISC_1:87;
then A26: [(o . ((y `1),(z `1))),(z `2)] in [:(o .: [:X,Y:]),Z:] by A25, ZFMISC_1:87;
x = o . ((y `1),(y `2)) by A17, MCART_1:21;
then x = o . ((o . ((y `1),(z `1))),(z `2)) by A2, A23;
hence x in o .: [:(o .: [:X,Y:]),Z:] by A1, A26, FUNCT_1:def 6; :: thesis: verum