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