consider L being Sequence such that
A2: ( dom L = succ 0 & ( 0 in succ 0 implies L . 0 = F2() ) & ( for A being Ordinal st succ A in succ 0 holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in succ 0 & A <> 0 & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) ) from ORDINAL2:sch 5();
 F2() = last L by A2, Th2, ORDINAL1:6;
hence F1(0) = F2() by A1, A2, ORDINAL1:6; :: thesis: verum