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;
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);
then consider f being Function of F₁(),F₂() such that
A3: for x being set st x in F₁() holds
f . x = F₃(x) ;
for x being Element of F₁() holds f . x = F₃(x) by A3;
hence ex f being Function of F₁(),F₂() st
for x being Element of F₁() holds f . x = F₃(x) ; :: thesis: verum