let Y, X be non empty set ; :: thesis: for F being BinOp of X
for f being Function of Y,X
for x being Element of X holds (F [:] (id X),x) * f = F [:] f,x
let F be BinOp of X; :: thesis: for f being Function of Y,X
for x being Element of X holds (F [:] (id X),x) * f = F [:] f,x
let f be Function of Y,X; :: thesis: for x being Element of X holds (F [:] (id X),x) * f = F [:] f,x
let x be Element of X; :: thesis: (F [:] (id X),x) * f = F [:] f,x
thus (F [:] (id X),x) * f = F [:] ((id X) * f),x by Th37
.= F [:] f,x by FUNCT_2:23 ; :: thesis: verum