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