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;
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);
then consider f being Function of F₁(),F₂() such that
A3: for x being object 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