let X be non empty set ; for Y being set
for F being BinOp of X
for f being Function of Y,X
for x1, x2 being Element of X st F is associative holds
F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2)))
let Y be set ; for F being BinOp of X
for f being Function of Y,X
for x1, x2 being Element of X st F is associative holds
F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2)))
let F be BinOp of X; for f being Function of Y,X
for x1, x2 being Element of X st F is associative holds
F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2)))
let f be Function of Y,X; for x1, x2 being Element of X st F is associative holds
F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2)))
let x1, x2 be Element of X; ( F is associative implies F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) )
assume A1:
F is associative
; F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2)))
per cases
( Y = {} or Y <> {} )
;
suppose A2:
Y <> {}
;
F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2)))now for y being Element of Y holds (F [:] ((F [;] (x1,f)),x2)) . y = F . (x1,((F [:] (f,x2)) . y))let y be
Element of
Y;
(F [:] ((F [;] (x1,f)),x2)) . y = F . (x1,((F [:] (f,x2)) . y))reconsider x3 =
f . y as
Element of
X by A2, FUNCT_2:5;
thus (F [:] ((F [;] (x1,f)),x2)) . y =
F . (
((F [;] (x1,f)) . y),
x2)
by A2, Th48
.=
F . (
(F . (x1,x3)),
x2)
by A2, Th53
.=
F . (
x1,
(F . (x3,x2)))
by A1
.=
F . (
x1,
((F [:] (f,x2)) . y))
by A2, Th48
;
verum end; hence
F [:] (
(F [;] (x1,f)),
x2)
= F [;] (
x1,
(F [:] (f,x2)))
by A2, Th54;
verum end; end;