let X be non empty set ; 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 ; 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; 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; for x being Element of X holds (F [;] (x,(id X))) * f = F [;] (x,f)
let x be Element of X; (F [;] (x,(id X))) * f = F [;] (x,f)
thus (F [;] (x,(id X))) * f =
F [;] (x,((id X) * f))
by Th34
.=
F [;] (x,f)
by FUNCT_2:17
; verum