let X, Y be non empty set ; :: thesis: for F being BinOp of X
for f being Function of Y,X
for g being Function of X,X holds (F .: ((id X),g)) * f = F .: (f,(g * f))
let F be BinOp of X; :: thesis: for f being Function of Y,X
for g being Function of X,X holds (F .: ((id X),g)) * f = F .: (f,(g * f))
let f be Function of Y,X; :: thesis: for g being Function of X,X holds (F .: ((id X),g)) * f = F .: (f,(g * f))
let g be Function of X,X; :: thesis: (F .: ((id X),g)) * f = F .: (f,(g * f))
thus (F .: ((id X),g)) * f = F .: (((id X) * f),(g * f)) by Th25
.= F .: (f,(g * f)) by FUNCT_2:17 ; :: thesis: verum