let A be Ordinal; :: thesis: ( A in dom F₁() implies F₁() . A = F₂(A) )
set fi = F₁() | (succ A);
assume A in dom F₁() ; :: thesis: F₁() . A = F₂(A)
then A6: succ A c= dom F₁() by ORDINAL1:21;
A7: 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 A8: succ C in succ A ; :: thesis: (F₁() | (succ A)) . (succ C) = F₅(C,((F₁() | (succ A)) . C))
C in succ C by ORDINAL1:6;
then A9: (F₁() | (succ A)) . C = F₁() . C by A8, FUNCT_1:49, ORDINAL1:10;
(F₁() | (succ A)) . (succ C) = F₁() . (succ C) by A8, FUNCT_1:49;
hence (F₁() | (succ A)) . (succ C) = F₅(C,((F₁() | (succ A)) . C)) by A2, A4, A6, A8, A9; :: thesis: verum

end;

A10: for C being Ordinal st C in succ A & C <> 0 & 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 <> 0 & C is limit_ordinal implies (F₁() | (succ A)) . C = F₆(C,((F₁() | (succ A)) | C)) )
assume that
A11: C in succ A and
A12: ( C <> 0 & C is limit_ordinal ) ; :: thesis: (F₁() | (succ A)) . C = F₆(C,((F₁() | (succ A)) | C))
C c= succ A by A11, ORDINAL1:def 2;
then A13: (F₁() | (succ A)) | C = F₁() | C by FUNCT_1:51;
(F₁() | (succ A)) . C = F₁() . C by A11, FUNCT_1:49;
hence (F₁() | (succ A)) . C = F₆(C,((F₁() | (succ A)) | C)) by A2, A5, A6, A11, A12, A13; :: thesis: verum

end;

0 c= succ A ;
then 0 c< succ A ;
then A14: ( 0 in succ A & (F₁() | (succ A)) . 0 = F₁() . 0 ) by FUNCT_1:49, ORDINAL1:11;
A15: dom (F₁() | (succ A)) = succ A by A6, RELAT_1:62;
then ( A in succ A & last (F₁() | (succ A)) = (F₁() | (succ A)) . A ) by Th2, ORDINAL1:21;
then last (F₁() | (succ A)) = F₁() . A by FUNCT_1:49;
hence F₁() . A = F₂(A) by A1, A2, A3, A6, A15, A14, A7, A10; :: thesis: verum