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