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 14 :: 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 set ; :: 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 set such that
A3: y in dom o and
A4: y in [:(o .: [:X,Y:]),Z:] and
A5: x = o . y by FUNCT_1:def 12;
reconsider y = y as Element of [:D,D:] by A3;
A6: y = [(y `1 ),(y `2 )] by MCART_1:23;
then A7: y `2 in Z by A4, ZFMISC_1:106;
y `1 in o .: [:X,Y:] by A4, A6, ZFMISC_1:106;
then consider z being set such that
A8: z in dom o and
A9: z in [:X,Y:] and
A10: y `1 = o . z by FUNCT_1:def 12;
reconsider z = z as Element of [:D,D:] by A8;
A11: y `1 = o . (z `1 ),(z `2 ) by A10, MCART_1:23;
A12: z = [(z `1 ),(z `2 )] by MCART_1:23;
then z `2 in Y by A9, ZFMISC_1:106;
then [(z `2 ),(y `2 )] in [:Y,Z:] by A7, ZFMISC_1:106;
then A13: o . (z `2 ),(y `2 ) in o .: [:Y,Z:] by A1, FUNCT_1:def 12;
z `1 in X by A9, A12, ZFMISC_1:106;
then A14: [(z `1 ),(o . (z `2 ),(y `2 ))] in [:X,(o .: [:Y,Z:]):] by A13, ZFMISC_1:106;
x = o . (y `1 ),(y `2 ) by A5, MCART_1:23;
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 12; :: thesis: verum

end;

let x be set ; :: 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 set such that
A15: y in dom o and
A16: y in [:X,(o .: [:Y,Z:]):] and
A17: x = o . y by FUNCT_1:def 12;
reconsider y = y as Element of [:D,D:] by A15;
A18: y = [(y `1 ),(y `2 )] by MCART_1:23;
then A19: y `1 in X by A16, ZFMISC_1:106;
y `2 in o .: [:Y,Z:] by A16, A18, ZFMISC_1:106;
then consider z being set such that
A20: z in dom o and
A21: z in [:Y,Z:] and
A22: y `2 = o . z by FUNCT_1:def 12;
reconsider z = z as Element of [:D,D:] by A20;
A23: y `2 = o . (z `1 ),(z `2 ) by A22, MCART_1:23;
A24: z = [(z `1 ),(z `2 )] by MCART_1:23;
then z `1 in Y by A21, ZFMISC_1:106;
then [(y `1 ),(z `1 )] in [:X,Y:] by A19, ZFMISC_1:106;
then A25: o . (y `1 ),(z `1 ) in o .: [:X,Y:] by A1, FUNCT_1:def 12;
z `2 in Z by A21, A24, ZFMISC_1:106;
then A26: [(o . (y `1 ),(z `1 )),(z `2 )] in [:(o .: [:X,Y:]),Z:] by A25, ZFMISC_1:106;
x = o . (y `1 ),(y `2 ) by A17, MCART_1:23;
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 12; :: thesis: verum