let X be non empty set ; for Y being set
for F being BinOp of X
for g being Function of Y,X
for x being Element of X holds F [;] (x,g) is Function of Y,X
let Y be set ; for F being BinOp of X
for g being Function of Y,X
for x being Element of X holds F [;] (x,g) is Function of Y,X
let F be BinOp of X; for g being Function of Y,X
for x being Element of X holds F [;] (x,g) is Function of Y,X
let g be Function of Y,X; for x being Element of X holds F [;] (x,g) is Function of Y,X
let x be Element of X; F [;] (x,g) is Function of Y,X
dom g = Y
by FUNCT_2:def 1;
then reconsider f = (dom g) --> x as Function of Y,X ;
F * <:f,g:> is Function of Y,X
;
hence
F [;] (x,g) is Function of Y,X
; verum