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 x being Element of X holds (F [;] x,(id X)) * f = F [;] x,f
let Y be set ; :: thesis: for F being BinOp of X
for f being Function of Y,X
for x being Element of X holds (F [;] x,(id X)) * f = F [;] x,f
let F be BinOp of X; :: thesis: for f being Function of Y,X
for x being Element of X holds (F [;] x,(id X)) * f = F [;] x,f
let f be Function of Y,X; :: thesis: for x being Element of X holds (F [;] x,(id X)) * f = F [;] x,f
let x be Element of X; :: thesis: (F [;] x,(id X)) * f = F [;] x,f
thus (F [;] x,(id X)) * f = F [;] x,((id X) * f) by Th44
.= F [;] x,f by FUNCT_2:23 ; :: thesis: verum