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 ;
y `1 in o .: [:X,Y:] by ;
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 ;
A12: z = [(z `1),(z `2)] by MCART_1:21;
then z `2 in Y by ;
then [(z `2),(y `2)] in [:Y,Z:] by ;
then A13: o . ((z `2),(y `2)) in o .: [:Y,Z:] by ;
z `1 in X by ;
then A14: [(z `1),(o . ((z `2),(y `2)))] in [:X,(o .: [:Y,Z:]):] by ;
x = o . ((y `1),(y `2)) by ;
then x = o . ((z `1),(o . ((z `2),(y `2)))) by ;
hence x in o .: [:X,(o .: [:Y,Z:]):] by ; :: 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 ;
y `2 in o .: [:Y,Z:] by ;
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 ;
A24: z = [(z `1),(z `2)] by MCART_1:21;
then z `1 in Y by ;
then [(y `1),(z `1)] in [:X,Y:] by ;
then A25: o . ((y `1),(z `1)) in o .: [:X,Y:] by ;
z `2 in Z by ;
then A26: [(o . ((y `1),(z `1))),(z `2)] in [:(o .: [:X,Y:]),Z:] by ;
x = o . ((y `1),(y `2)) by ;
then x = o . ((o . ((y `1),(z `1))),(z `2)) by ;
hence x in o .: [:(o .: [:X,Y:]),Z:] by ; :: thesis: verum