let A be Ordinal; ( A in dom F1() implies F1() . A = F2(A) )
set fi = F1() | (succ A);
assume
A in dom F1()
; 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;
( succ C in succ A implies (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C)) )
assume A8:
succ C in succ A
;
(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;
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;
( 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 )
;
(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;
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; verum