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