consider L being Sequence such that
F2((dom F1())) = F3(L) and
A3: dom L = dom F1() and
A4: for B being Ordinal st B in dom F1() holds
L . B = F3((L | B)) by A1;
now :: thesis: for b being object st b in dom L holds
F1() . b = L . b
let b be object ; :: thesis: ( b in dom L implies F1() . b = L . b )
assume A5: b in dom L ; :: thesis: F1() . b = L . b
then reconsider B = b as Ordinal by Th9;
now :: thesis: ex K being number st
( F3((L | B)) = F3(K) & dom K = B & ( for C being Ordinal st C in B holds
K . C = F3((K | C)) ) )
take K = L | B; :: thesis: ( F3((L | B)) = F3(K) & dom K = B & ( for C being Ordinal st C in B holds
K . C = F3((K | C)) ) )
thus F3((L | B)) = F3(K) ; :: thesis: ( dom K = B & ( for C being Ordinal st C in B holds
K . C = F3((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 = F3((K | C))
let C be Ordinal; :: thesis: ( C in B implies K . C = F3((K | C)) )
assume A7: C in B ; :: thesis: K . C = F3((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 = F3((K | C)) by A3, A4, A6, A7, A8; :: thesis: verum
end;
then F2(B) = F3((L | B)) by A1
.= L . B by A3, A4, A5 ;
hence F1() . b = L . b by A2, A3, A5; :: thesis: verum
end;
then F1() = L by A3;
hence for B being Ordinal st B in dom F1() holds
F1() . B = F3((F1() | B)) by A4; :: thesis: verum