let C be Ordinal; for phi being Ordinal-Sequence st phi is increasing & phi is continuous holds
C +^ phi is continuous
let phi be Ordinal-Sequence; ( phi is increasing & phi is continuous implies C +^ phi is continuous )
assume A1:
phi is increasing
; ( not phi is continuous or C +^ phi is continuous )
assume A2:
for A, B being Ordinal st A in dom phi & A <> 0 & A is limit_ordinal & B = phi . A holds
B is_limes_of phi | A
; ORDINAL2:def 13 C +^ phi is continuous
let A be Ordinal; ORDINAL2:def 13 for b1 being set holds
( not A in dom (C +^ phi) or A = 0 or not A is limit_ordinal or not b1 = (C +^ phi) . A or b1 is_limes_of (C +^ phi) | A )
let B be Ordinal; ( not A in dom (C +^ phi) or A = 0 or not A is limit_ordinal or not B = (C +^ phi) . A or B is_limes_of (C +^ phi) | A )
set xi = phi | A;
reconsider A9 = phi . A as Ordinal ;
assume that
A3:
A in dom (C +^ phi)
and
A4:
A <> 0
and
A5:
A is limit_ordinal
and
A6:
B = (C +^ phi) . A
; B is_limes_of (C +^ phi) | A
A7:
dom phi = dom (C +^ phi)
by ORDINAL3:def 1;
then A8:
B = C +^ A9
by A3, A6, ORDINAL3:def 1;
A9 is_limes_of phi | A
by A2, A3, A4, A5, A7;
then A9:
lim (phi | A) = A9
by ORDINAL2:def 10;
A10:
( dom (phi | A) = dom (C +^ (phi | A)) & (C +^ phi) | A = C +^ (phi | A) )
by Th15, ORDINAL3:def 1;
A11:
phi | A is increasing
by A1, ORDINAL4:15;
then A12:
C +^ (phi | A) is increasing
by Th14;
A c= dom (C +^ phi)
by A3, ORDINAL1:def 2;
then A13:
dom (phi | A) = A
by A7, RELAT_1:62;
then A14:
sup (C +^ (phi | A)) = C +^ (sup (phi | A))
by A4, ORDINAL3:43;
sup (phi | A) = lim (phi | A)
by A4, A5, A13, A11, ORDINAL4:8;
hence
B is_limes_of (C +^ phi) | A
by A4, A5, A13, A10, A8, A14, A9, A12, ORDINAL4:8; verum