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