let A be Ordinal; :: thesis: ( A in dom F₁() implies F₁() . A = F₂(A) )
set L = F₁() | (succ A);
assume A in dom F₁() ; :: thesis: F₁() . A = F₂(A)
then A6: ( succ A c= dom F₁() & A in succ A ) by ORDINAL1:33;
then A7: dom (F₁() | (succ A)) = succ A by RELAT_1:91;
then last (F₁() | (succ A)) = (F₁() | (succ A)) . A by Th2;
then A8: last (F₁() | (succ A)) = F₁() . A by A6, FUNCT_1:72;
( succ A <> {} & {} c= succ A ) ;
then {} c< succ A by XBOOLE_0:def 8;
then {} in succ A by ORDINAL1:21;
then A9: ( F₁() . {} = F₄() & (F₁() | (succ A)) . {} = F₁() . {} ) by A2, A3, A6, FUNCT_1:72;
A10: for C being Ordinal st succ C in succ A holds
(F₁() | (succ A)) . (succ C) = F₅(C,((F₁() | (succ A)) . C))

proof

let C be Ordinal; :: thesis: ( succ C in succ A implies (F₁() | (succ A)) . (succ C) = F₅(C,((F₁() | (succ A)) . C)) )
assume A11: succ C in succ A ; :: thesis: (F₁() | (succ A)) . (succ C) = F₅(C,((F₁() | (succ A)) . C))
C in succ C by ORDINAL1:10;
then ( (F₁() | (succ A)) . C = F₁() . C & (F₁() | (succ A)) . (succ C) = F₁() . (succ C) ) by A11, FUNCT_1:72, ORDINAL1:19;
hence (F₁() | (succ A)) . (succ C) = F₅(C,((F₁() | (succ A)) . C)) by A2, A4, A6, A11; :: thesis: verum

end;

for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
(F₁() | (succ A)) . C = F₆(C,((F₁() | (succ A)) | C))

proof

let C be Ordinal; :: thesis: ( C in succ A & C <> {} & C is limit_ordinal implies (F₁() | (succ A)) . C = F₆(C,((F₁() | (succ A)) | C)) )
assume A12: ( C in succ A & C <> {} & C is limit_ordinal ) ; :: thesis: (F₁() | (succ A)) . C = F₆(C,((F₁() | (succ A)) | C))
then ( C in F₃() & C c= succ A ) by A2, A6, ORDINAL1:def 2;
then ( (F₁() | (succ A)) . C = F₁() . C & (F₁() | (succ A)) | C = F₁() | C ) by A12, FUNCT_1:72, FUNCT_1:82;
hence (F₁() | (succ A)) . C = F₆(C,((F₁() | (succ A)) | C)) by A2, A5, A6, A12; :: thesis: verum

end;

hence F₁() . A = F₂(A) by A1, A7, A8, A9, A10; :: thesis: verum