defpred S₁[ Nat, set , set ] means $3 = F₂($1,$2);
A7: for n being Nat holds S₁[n,F₄() . n,F₄() . (succ n)] by A6;
A8: for n being Nat
for x, y1, y2 being set st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2 ;
A9: for n being Nat holds S₁[n,F₃() . n,F₃() . (succ n)] by A3;
thus F₃() = F₄() from ORDINAL2:sch 19(A1, A2, A9, A4, A5, A7, A8); :: thesis: verum