defpred S₁[ set , set , set ] means $3 = F₄($1,$2);
A2: for x, y being set st x in F₁() & y in F₂() holds
ex z being set st
( z in F₃() & S₁[x,y,z] ) by A1;
thus ex f being Function of [:F₁(),F₂():],F₃() st
for x, y being set st x in F₁() & y in F₂() holds
S₁[x,y,f . (x,y)] from BINOP_1:sch 1(A2); :: thesis: verum