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 .: (g,(id X))) * f = F .: ((g * f),f)

let F be BinOp of X; :: thesis: for f being Function of Y,X

for g being Function of X,X holds (F .: (g,(id X))) * f = F .: ((g * f),f)

let f be Function of Y,X; :: thesis: for g being Function of X,X holds (F .: (g,(id X))) * f = F .: ((g * f),f)

let g be Function of X,X; :: thesis: (F .: (g,(id X))) * f = F .: ((g * f),f)

thus (F .: (g,(id X))) * f = F .: ((g * f),((id X) * f)) by Th25

.= F .: ((g * f),f) by FUNCT_2:17 ; :: thesis: verum

for f being Function of Y,X

for g being Function of X,X holds (F .: (g,(id X))) * f = F .: ((g * f),f)

let F be BinOp of X; :: thesis: for f being Function of Y,X

for g being Function of X,X holds (F .: (g,(id X))) * f = F .: ((g * f),f)

let f be Function of Y,X; :: thesis: for g being Function of X,X holds (F .: (g,(id X))) * f = F .: ((g * f),f)

let g be Function of X,X; :: thesis: (F .: (g,(id X))) * f = F .: ((g * f),f)

thus (F .: (g,(id X))) * f = F .: ((g * f),((id X) * f)) by Th25

.= F .: ((g * f),f) by FUNCT_2:17 ; :: thesis: verum