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)

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

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

hence F [;] (F . x1,x2),f = F [;] x1,(F [;] x2,f) ; :: thesis: verum

end;

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

now

let 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:7;
thus (F [;] (F . x1,x2),f) . y = F . (F . x1,x2),(f . y) by A2, Th66
.= F . x1,(F . x2,x3) by A1, BINOP_1:def 3
.= F . x1,((F [;] x2,f) . y) by A2, Th66 ; :: thesis: verum

end;

hence F [;] (F . x1,x2),f = F [;] x1,(F [;] x2,f) by A2, Th67; :: thesis: verum

end;

end;