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