let C be Ordinal; :: thesis: for phi being Ordinal-Sequence st phi is increasing & phi is continuous holds
C +^ phi is continuous
let phi be Ordinal-Sequence; :: thesis: ( phi is increasing & phi is continuous implies C +^ phi is continuous )
assume A1: phi is increasing ; :: thesis: ( not phi is continuous or C +^ phi is continuous )
assume A2: for A, B being Ordinal st A in dom phi & A <> {} & A is limit_ordinal & B = phi . A holds
B is_limes_of phi | A ; :: according to ORDINAL2:def 17 :: thesis: C +^ phi is continuous
let A be Ordinal; :: according to ORDINAL2:def 17 :: thesis: for b₁ being set holds
( not A in proj1 (C +^ phi) or A = {} or not A is limit_ordinal or not b₁ = (C +^ phi) . A or b₁ is_limes_of (C +^ phi) | A )
let B be Ordinal; :: thesis: ( not A in proj1 (C +^ phi) or A = {} or not A is limit_ordinal or not B = (C +^ phi) . A or B is_limes_of (C +^ phi) | A )
set xi = phi | A;
assume A3: ( A in dom (C +^ phi) & A <> {} & A is limit_ordinal & B = (C +^ phi) . A ) ; :: thesis: B is_limes_of (C +^ phi) | A
then A4: ( A c= dom (C +^ phi) & dom phi = dom (C +^ phi) & dom (phi | A) = dom (C +^ (phi | A)) ) by ORDINAL1:def 2, ORDINAL3:def 2;
reconsider A' = phi . A as Ordinal ;
A5: ( A' is_limes_of phi | A & dom (phi | A) = A & (C +^ phi) | A = C +^ (phi | A) & B = C +^ A' ) by A2, A3, A4, Th16, ORDINAL3:def 2, RELAT_1:91;
then A6: ( sup (C +^ (phi | A)) = C +^ (sup (phi | A)) & lim (phi | A) = A' & phi | A is increasing ) by A1, A3, ORDINAL2:def 14, ORDINAL3:51, ORDINAL4:15;
then ( C +^ (phi | A) is increasing & sup (phi | A) = lim (phi | A) ) by A3, A5, Th15, ORDINAL4:8;
hence B is_limes_of (C +^ phi) | A by A3, A4, A5, A6, ORDINAL4:8; :: thesis: verum