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