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