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