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:]

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

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 .: [:X,(o .: [:Y,Z:]):] or x in o .: [:(o .: [:X,Y:]),Z:] )
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;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

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