A2: for t being Element of F₁() st t in F₃() holds
ex ff being Element of F₂() st P₁[t,ff] by A1;
consider ff being Function of F₁(),F₂() such that
A3: for t being Element of F₁() st t in F₃() holds
P₁[t,ff . t] from FRAENKEL:sch 26(A2);
reconsider ff = ff as Element of Funcs (F₁(),F₂()) by FUNCT_2:8;
take ff ; :: thesis: for t being Element of F₁() st t in F₃() holds
P₁[t,ff . t]
thus for t being Element of F₁() st t in F₃() holds
P₁[t,ff . t] by A3; :: thesis: verum