set A = F1();
deffunc H1( Element of F1(), Element of F1()) -> Element of F1() = In (F2($1,$2),F1());
ex f being Function of [:F1(),F1():],F1() st
for x, y being Element of F1() holds f . (x,y) = H1(x,y) from BINOP_1:sch 4();
 then consider f being BinOp of F1() such that
A1: for x, y being Element of F1() holds f . (x,y) = H1(x,y) ;
take f ; :: thesis: for a, b being Element of F1() holds f . (a,b) = F2(a,b)
let a, b be Element of F1(); :: thesis: f . (a,b) = F2(a,b)
f . (a,b) = H1(a,b) by A1;
hence f . (a,b) = F2(a,b) by SUBSET_1:def 8, A2; :: thesis: verum