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