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