defpred S1[ object , object , object ] means $3 = F3($1,$2);
A1:
for x, y being object st x in F1() & y in F2() holds
ex z being object st S1[x,y,z]
;
A2:
for x, y, z1, z2 being object st x in F1() & y in F2() & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2
;
ex f being Function st
( dom f = [:F1(),F2():] & ( for x, y being object st x in F1() & y in F2() holds
S1[x,y,f . (x,y)] ) )
from FUNCT_3:sch 1(A2, A1);
hence
ex f being Function st
( dom f = [:F1(),F2():] & ( for x, y being object st x in F1() & y in F2() holds
f . (x,y) = F3(x,y) ) )
; verum