consider L being T-Sequence such that
A2: ( dom L = succ {} & ( {} in succ {} implies L . {} = F₂() ) & ( for A being Ordinal st succ A in succ {} holds
L . (succ A) = F₃(A,(L . A)) ) & ( for A being Ordinal st A in succ {} & A <> {} & A is limit_ordinal holds
L . A = F₄(A,(L | A)) ) ) from ORDINAL2:sch 5();
( F₂() = last L & L . {} = F₂() ) by A2, Th2, ORDINAL1:10;
hence F₁({} ) = F₂() by A1, A2; :: thesis: verum