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