A5: F2() in succ F2() by ORDINAL1:6;
consider L being Sequence such that
A6: dom L = succ F2() and
A7: ( 0 in succ F2() implies L . 0 = F4() ) and
A8: for C being Ordinal st succ C in succ F2() holds
L . (succ C) = F5(C,(L . C)) and
A9: for C being Ordinal st C in succ F2() & C <> 0 & C is limit_ordinal holds
L . C = F6(C,(L | C)) from ORDINAL2:sch 5();
 set L1 = L | F2();
A10: for A being Ordinal
for x being object holds
( x = F3(A) iff ex L being Sequence st
( x = last L & dom L = succ A & L . 0 = F4() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) by A1;
A11: for B being Ordinal st B in dom L holds
L . B = F3(B) from ORDINAL2:sch 6(A10, A6, A7, A8, A9);
A12: now :: thesis: for x being object st x in F2() holds
(L | F2()) . x = F1() . x
let x be object ; :: thesis: ( x in F2() implies (L | F2()) . x = F1() . x )
assume A13: x in F2() ; :: thesis: (L | F2()) . x = F1() . x
then reconsider x9 = x as Ordinal ;
thus (L | F2()) . x = L . x9 by A13, FUNCT_1:49
.= F3(x9) by A6, A11, A5, A13, ORDINAL1:10
.= F1() . x by A4, A13 ; :: thesis: verum
end;
F2() c= dom L by A6, A5, ORDINAL1:def 2;
then dom (L | F2()) = F2() by RELAT_1:62;
then L | F2() = F1() by A3, A12, FUNCT_1:2;
then L . F2() = F6(F2(),F1()) by A2, A9, ORDINAL1:6;
hence F3(F2()) = F6(F2(),F1()) by A6, A11, ORDINAL1:6; :: thesis: verum