defpred S₁[ Nat, set , set ] means $3 = F₃($1,$2);
A5: for n being Nat holds S₁[n,F₅() . n,F₅() . (n + 1)] by A4;
A6: for n being Nat
for x, y1, y2 being Element of F₁() st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2 ;
A7: for n being Nat holds S₁[n,F₄() . n,F₄() . (n + 1)] by A2;
thus F₄() = F₅() from NAT_1:sch 14(A1, A7, A3, A5, A6); :: thesis: verum