let A be Ordinal; F4((succ A)) = F2(A,F4(A))
consider L being T-Sequence such that
A2:
dom L = succ (succ A)
and
A3:
( {} in succ (succ A) implies L . {} = F1() )
and
A4:
for C being Ordinal st succ C in succ (succ A) holds
L . (succ C) = F2(C,(L . C))
and
A5:
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();
A6:
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;
A7:
for B being Ordinal st B in dom L holds
L . B = F4(B)
from ORDINAL2:sch 6(A6, A2, A3, A4, A5);
then A8:
L . (succ A) = F4((succ A))
by A2, ORDINAL1:6;
( A in succ A & succ A in succ (succ A) )
by ORDINAL1:6;
then
L . A = F4(A)
by A2, A7, ORDINAL1:10;
hence
F4((succ A)) = F2(A,F4(A))
by A4, A8, ORDINAL1:6; verum