let X be non empty set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: for x being Element of X holds F [;] (x,g) is Function of Y,X

let x be Element of X; :: thesis: 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 ; :: thesis: verum

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 ; :: thesis: 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; :: thesis: 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; :: thesis: for x being Element of X holds F [;] (x,g) is Function of Y,X

let x be Element of X; :: thesis: 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 ; :: thesis: verum