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,f)),x2) = F [;] (x1,(F [:] (f,x2)))
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,f)),x2) = F [;] (x1,(F [:] (f,x2)))
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,f)),x2) = F [;] (x1,(F [:] (f,x2)))
let f be Function of Y,X; :: thesis: 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; :: thesis: ( F is associative implies F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) )
assume A1: F is associative ; :: thesis: F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2)))

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

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

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

end;

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

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

end;

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

end;

end;