let X, Y 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 Th29

.= F [:] (f,x) by FUNCT_2:17 ; :: thesis: verum

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 Th29

.= F [:] (f,x) by FUNCT_2:17 ; :: thesis: verum