consider L being Sequence such that
F₂((dom F₁())) = F₃(L) and
A3: dom L = dom F₁() and
A4: for B being Ordinal st B in dom F₁() holds
L . B = F₃((L | B)) by A1;

now :: thesis: for b being object st b in dom L holds
F₁() . b = L . b

let b be object ; :: thesis: ( b in dom L implies F₁() . b = L . b )
assume A5: b in dom L ; :: thesis: F₁() . b = L . b
then reconsider B = b as Ordinal by Th9;

now :: thesis: ex K being number st
( F₃((L | B)) = F₃(K) & dom K = B & ( for C being Ordinal st C in B holds
K . C = F₃((K | C)) ) )

take K = L | B; :: thesis: ( F₃((L | B)) = F₃(K) & dom K = B & ( for C being Ordinal st C in B holds
K . C = F₃((K | C)) ) )
thus F₃((L | B)) = F₃(K) ; :: thesis: ( dom K = B & ( for C being Ordinal st C in B holds
K . C = F₃((K | C)) ) )
A6: B c= dom L by A5, Def2;
hence dom K = B by RELAT_1:62; :: thesis: for C being Ordinal st C in B holds
K . C = F₃((K | C))
let C be Ordinal; :: thesis: ( C in B implies K . C = F₃((K | C)) )
assume A7: C in B ; :: thesis: K . C = F₃((K | C))
then C c= B by Def2;
then A8: L | C = K | C by FUNCT_1:51;
K . C = L . C by A7, FUNCT_1:49;
hence K . C = F₃((K | C)) by A3, A4, A6, A7, A8; :: thesis: verum

end;

then F₂(B) = F₃((L | B)) by A1
.= L . B by A3, A4, A5 ;
hence F₁() . b = L . b by A2, A3, A5; :: thesis: verum

end;

then F₁() = L by A3;
hence for B being Ordinal st B in dom F₁() holds
F₁() . B = F₃((F₁() | B)) by A4; :: thesis: verum