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

now

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

end;

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