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 Th34

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

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 Th34

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