let A be Ordinal; :: thesis: ( A in dom F1() implies F1() . A = F2(A) )
set L = F1() | (succ A);
assume A in dom F1() ; :: thesis: F1() . A = F2(A)
then A6: succ A c= dom F1() by ORDINAL1:21;
A7: for C being Ordinal st succ C in succ A holds
(F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C))
proof
let C be Ordinal; :: thesis: ( succ C in succ A implies (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C)) )
assume A8: succ C in succ A ; :: thesis: (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C))
C in succ C by ORDINAL1:6;
then A9: (F1() | (succ A)) . C = F1() . C by A8, FUNCT_1:49, ORDINAL1:10;
(F1() | (succ A)) . (succ C) = F1() . (succ C) by A8, FUNCT_1:49;
hence (F1() | (succ A)) . (succ C) = F5(C,((F1() | (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
(F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C))
proof
let C be Ordinal; :: thesis: ( C in succ A & C <> 0 & C is limit_ordinal implies (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C)) )
assume that
A11: C in succ A and
A12: ( C <> 0 & C is limit_ordinal ) ; :: thesis: (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C))
C c= succ A by A11, ORDINAL1:def 2;
then A13: (F1() | (succ A)) | C = F1() | C by FUNCT_1:51;
(F1() | (succ A)) . C = F1() . C by A11, FUNCT_1:49;
hence (F1() | (succ A)) . C = F6(C,((F1() | (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 & (F1() | (succ A)) . 0 = F1() . 0 ) by FUNCT_1:49, ORDINAL1:11;
A15: dom (F1() | (succ A)) = succ A by A6, RELAT_1:62;
then ( A in succ A & last (F1() | (succ A)) = (F1() | (succ A)) . A ) by Th2, ORDINAL1:21;
then last (F1() | (succ A)) = F1() . A by FUNCT_1:49;
hence F1() . A = F2(A) by A1, A2, A3, A6, A15, A14, A7, A10; :: thesis: verum