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