let A be Ordinal; :: thesis: F4((succ A)) = F2(A,F4(A))
consider fi being Ordinal-Sequence such that
A2: dom fi = succ (succ A) and
A3: ( 0 in succ (succ A) implies fi . 0 = F1() ) and
A4: for C being Ordinal st succ C in succ (succ A) holds
fi . (succ C) = F2(C,(fi . C)) and
A5: for C being Ordinal st C in succ (succ A) & C <> 0 & C is limit_ordinal holds
fi . C = F3(C,(fi | C)) from ORDINAL2:sch 11();
 A6: for A, B being Ordinal holds
( B = F4(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . 0 = F1() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F2(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = F3(C,(fi | C)) ) ) ) by A1;
A7: for B being Ordinal st B in dom fi holds
fi . B = F4(B) from ORDINAL2:sch 12(A6, A2, A3, A4, A5);
 then A8: fi . (succ A) = F4((succ A)) by A2, ORDINAL1:6;
( A in succ A & succ A in succ (succ A) ) by ORDINAL1:6;
then fi . A = F4(A) by A2, A7, ORDINAL1:10;
hence F4((succ A)) = F2(A,F4(A)) by A4, A8, ORDINAL1:6; :: thesis: verum