defpred S1[ Integer, Integer, set ] means $3 = F1($1,$2);
A1:
for x, y being Element of INT ex z being Element of INT st S1[x,y,z]
consider f being Function of [:INT,INT:],INT such that
A2:
for x, y being Element of INT holds S1[x,y,f . (x,y)]
from BINOP_1:sch 3(A1);
take
f
; for x, y being Integer holds f . (x,y) = F1(x,y)
let x, y be Integer; f . (x,y) = F1(x,y)
reconsider x = x, y = y as Element of INT by INT_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