let X be non empty set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( F is associative implies F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) )

assume A1: F is associative ; :: thesis: F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f)))

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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( F is associative implies F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) )

assume A1: F is associative ; :: thesis: F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f)))

per cases
( Y = {} or Y <> {} )
;

end;

suppose A2:
Y <> {}
; :: thesis: F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f)))

end;

now :: thesis: for y being Element of Y holds (F [;] ((F . (x1,x2)),f)) . y = F . (x1,((F [;] (x2,f)) . y))

hence
F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f)))
by A2, Th54; :: thesis: verumlet y be Element of Y; :: thesis: (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 ; :: thesis: verum

end;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 ; :: thesis: verum