let X, Y, Z be set ; 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 ; 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; ( 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)))
; BINOP_1:def 3 o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):]
thus
o .: [:(o .: [:X,Y:]),Z:] c= o .: [:X,(o .: [:Y,Z:]):]
XBOOLE_0:def 10 o .: [:X,(o .: [:Y,Z:]):] c= o .: [:(o .: [:X,Y:]),Z:]proof
let x be
object ;
TARSKI:def 3 ( not x in o .: [:(o .: [:X,Y:]),Z:] or x in o .: [:X,(o .: [:Y,Z:]):] )
assume
x in o .: [:(o .: [:X,Y:]),Z:]
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( not x in o .: [:X,(o .: [:Y,Z:]):] or x in o .: [:(o .: [:X,Y:]),Z:] )
assume
x in o .: [:X,(o .: [:Y,Z:]):]
; 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; verum