consider fi being Ordinal-Sequence such that
A2: ( dom fi = succ 0 & ( 0 in succ 0 implies fi . 0 = F2() ) & ( for A being Ordinal st succ A in succ 0 holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in succ 0 & A <> 0 & 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(0) = F2() by A1, A2, ORDINAL1:6; :: thesis: verum