let A be Ordinal; :: thesis: F₄((succ A)) = F₂(A,F₄(A))
consider L being Sequence such that
A2: dom L = succ (succ A) and
A3: ( 0 in succ (succ A) implies L . 0 = F₁() ) and
A4: for C being Ordinal st succ C in succ (succ A) holds
L . (succ C) = F₂(C,(L . C)) and
A5: for C being Ordinal st C in succ (succ A) & C <> 0 & C is limit_ordinal holds
L . C = F₃(C,(L | C)) from ORDINAL2:sch 5();
A6: for A being Ordinal
for x being object holds
( x = F₄(A) iff ex L being Sequence st
( x = last L & dom L = succ A & L . 0 = F₁() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₂(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = F₃(C,(L | C)) ) ) ) by A1;
A7: for B being Ordinal st B in dom L holds
L . B = F₄(B) from ORDINAL2:sch 6(A6, A2, A3, A4, A5);
then A8: L . (succ A) = F₄((succ A)) by A2, ORDINAL1:6;
( A in succ A & succ A in succ (succ A) ) by ORDINAL1:6;
then L . A = F₄(A) by A2, A7, ORDINAL1:10;
hence F₄((succ A)) = F₂(A,F₄(A)) by A4, A8, ORDINAL1:6; :: thesis: verum