defpred S1[ Real, Real, set ] means $3 = F1($1,$2);
A1:
for x, y being Element of REAL ex z being Element of REAL st S1[x,y,z]
consider f being Function of [:REAL,REAL:],REAL such that
A2:
for x, y being Element of REAL holds S1[x,y,f . (x,y)]
from BINOP_1:sch 3(A1);
take
f
; for x, y being Real holds f . (x,y) = F1(x,y)
let x, y be Real; f . (x,y) = F1(x,y)
reconsider x = x, y = y as Element of REAL by XREAL_0:def 1;
S1[x,y,f . (x,y)]
by A2;
then
f . (x,y) = F1(x,y)
;
hence
f . (x,y) = F1(x,y)
; verum