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