A5: for A, B being Ordinal holds
( B = F₃(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F₄() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F₅(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F₆(C,(fi | C)) ) ) ) by A1;
consider fi being Ordinal-Sequence such that
A6: dom fi = succ F₂() and
A7: ( {} in succ F₂() implies fi . {} = F₄() ) and
A8: for C being Ordinal st succ C in succ F₂() holds
fi . (succ C) = F₅(C,(fi . C)) and
A9: for C being Ordinal st C in succ F₂() & C <> {} & C is limit_ordinal holds
fi . C = F₆(C,(fi | C)) from ORDINAL2:sch 11();
A10: for B being Ordinal st B in dom fi holds
fi . B = F₃(B) from ORDINAL2:sch 12(A5, A6, A7, A8, A9);
set psi = fi | F₂();
A11: F₂() in succ F₂() by ORDINAL1:10;
then F₂() c= dom fi by A6, ORDINAL1:def 2;
then A12: dom (fi | F₂()) = F₂() by RELAT_1:91;

now

let x be set ; :: thesis: ( x in F₂() implies (fi | F₂()) . x = F₁() . x )
assume A13: x in F₂() ; :: thesis: (fi | F₂()) . x = F₁() . x
then reconsider x' = x as Ordinal ;
thus (fi | F₂()) . x = fi . x' by A13, FUNCT_1:72
.= F₃(x') by A6, A10, A11, A13, ORDINAL1:19
.= F₁() . x by A4, A13 ; :: thesis: verum

end;

then fi | F₂() = F₁() by A3, A12, FUNCT_1:9;
then fi . F₂() = F₆(F₂(),F₁()) by A2, A9, ORDINAL1:10;
hence F₃(F₂()) = F₆(F₂(),F₁()) by A6, A10, ORDINAL1:10; :: thesis: verum