let g be Ordinal-Sequence-valued Sequence; :: thesis: ( dom g <> {} & ( for a being Ordinal st a in dom g holds
g . a is normal ) implies criticals g is continuous )
assume A1: dom g <> {} ; :: thesis: ( ex a being Ordinal st
( a in dom g & not g . a is normal ) or criticals g is continuous )
assume A2: for a being Ordinal st a in dom g holds
g . a is normal ; :: thesis: criticals g is continuous
set f = criticals g;
let a be Ordinal; :: according to ORDINAL2:def 13 :: thesis: for b₁ being set holds
( not a in dom (criticals g) or a = 0 or not a is limit_ordinal or not b₁ = (criticals g) . a or b₁ is_limes_of (criticals g) | a )
let b be Ordinal; :: thesis: ( not a in dom (criticals g) or a = 0 or not a is limit_ordinal or not b = (criticals g) . a or b is_limes_of (criticals g) | a )
reconsider h = (criticals g) | a as increasing Ordinal-Sequence by ORDINAL4:15;
assume A3: ( a in dom (criticals g) & a <> 0 & a is limit_ordinal & b = (criticals g) . a ) ; :: thesis: b is_limes_of (criticals g) | a
then A4: b = Union h by A1, A2, Th52;
a c= dom (criticals g) by A3, ORDINAL1:def 2;
then dom h = a by RELAT_1:62;
hence b is_limes_of (criticals g) | a by A3, A4, ORDINAL5:6; :: thesis: verum