A5: F₂() in succ F₂() by ORDINAL1:6;
consider fi being Ordinal-Sequence such that
A6: dom fi = succ F₂() and
A7: ( 0 in succ F₂() implies fi . 0 = 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 <> 0 & C is limit_ordinal holds
fi . C = F₆(C,(fi | C)) from ORDINAL2:sch 11();
set psi = fi | F₂();
A10: for A, B being Ordinal holds
( B = F₃(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . 0 = 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 <> 0 & C is limit_ordinal holds
fi . C = F₆(C,(fi | C)) ) ) ) by A1;
A11: for B being Ordinal st B in dom fi holds
fi . B = F₃(B) from ORDINAL2:sch 12(A10, A6, A7, A8, A9);

A12: now :: thesis: for x being object st x in F₂() holds
(fi | F₂()) . x = F₁() . x

let x be object ; :: thesis: ( x in F₂() implies (fi | F₂()) . x = F₁() . x )
assume A13: x in F₂() ; :: thesis: (fi | F₂()) . x = F₁() . x
then reconsider x9 = x as Ordinal ;
thus (fi | F₂()) . x = fi . x9 by A13, FUNCT_1:49
.= F₃(x9) by A6, A11, A5, A13, ORDINAL1:10
.= F₁() . x by A4, A13 ; :: thesis: verum

end;

F₂() c= dom fi by A6, A5, ORDINAL1:def 2;
then dom (fi | F₂()) = F₂() by RELAT_1:62;
then fi | F₂() = F₁() by A3, A12, FUNCT_1:2;
then fi . F₂() = F₆(F₂(),F₁()) by A2, A9, ORDINAL1:6;
hence F₃(F₂()) = F₆(F₂(),F₁()) by A6, A11, ORDINAL1:6; :: thesis: verum