let X be non empty set ; :: thesis: for Y being set
for F being BinOp of X
for f, g being Function of Y,X holds F .: (f,g) is Function of Y,X
let Y be set ; :: thesis: for F being BinOp of X
for f, g being Function of Y,X holds F .: (f,g) is Function of Y,X
let F be BinOp of X; :: thesis: for f, g being Function of Y,X holds F .: (f,g) is Function of Y,X
let f, g be Function of Y,X; :: thesis: F .: (f,g) is Function of Y,X
F * <:f,g:> is Function of Y,X ;
hence F .: (f,g) is Function of Y,X ; :: thesis: verum