set A = F_{1}();

deffunc H_{1}( Element of F_{1}(), Element of F_{1}()) -> Element of F_{1}() = In (F_{2}($1,$2),F_{1}());

ex f being Function of [:F_{1}(),F_{1}():],F_{1}() st

for x, y being Element of F_{1}() holds f . (x,y) = H_{1}(x,y)
from BINOP_1:sch 4();

then consider f being BinOp of F_{1}() such that

A1: for x, y being Element of F_{1}() holds f . (x,y) = H_{1}(x,y)
;

take f ; :: thesis: for a, b being Element of F_{1}() holds f . (a,b) = F_{2}(a,b)

let a, b be Element of F_{1}(); :: thesis: f . (a,b) = F_{2}(a,b)

f . (a,b) = H_{1}(a,b)
by A1;

hence f . (a,b) = F_{2}(a,b)
by SUBSET_1:def 8, A2; :: thesis: verum

deffunc H

ex f being Function of [:F

for x, y being Element of F

then consider f being BinOp of F

A1: for x, y being Element of F

take f ; :: thesis: for a, b being Element of F

let a, b be Element of F

f . (a,b) = H

hence f . (a,b) = F