let Y, X be non empty set ; :: thesis: 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; :: thesis: for f being Function of Y,X holds (F .: (id X),(id X)) * f = F .: f,f
let f be Function of Y,X; :: thesis: (F .: (id X),(id X)) * f = F .: f,f
thus (F .: (id X),(id X)) * f = F .: ((id X) * f),((id X) * f) by Th31
.= F .: ((id X) * f),f by FUNCT_2:23
.= F .: f,f by FUNCT_2:23 ; :: thesis: verum