let f be Ordinal-Sequence; :: thesis: ( f is normal implies for a being Ordinal st a in dom (criticals f) holds
f . a c= (criticals f) . a )
assume A1: f is normal ; :: thesis: for a being Ordinal st a in dom (criticals f) holds
f . a c= (criticals f) . a
set g = criticals f;
A2: dom (criticals f) c= dom f by Th32;
defpred S1[ Ordinal] means ( $1 in dom (criticals f) implies f . $1 c= (criticals f) . $1 );
A3: S1[ 0 ]
proof
assume 0 in dom (criticals f) ; :: thesis: f . 0 c= (criticals f) . 0
then (criticals f) . 0 is_a_fixpoint_of f by Th29;
then ( f . ((criticals f) . 0) = (criticals f) . 0 & (criticals f) . 0 in dom f ) ;
hence f . 0 c= (criticals f) . 0 by A1, ORDINAL4:9, XBOOLE_1:2; :: thesis: verum
end;
A4: for a being Ordinal st S1[a] holds
S1[ succ a]
proof
let a be Ordinal; :: thesis: ( S1[a] implies S1[ succ a] )
assume that
S1[a] and
A5: succ a in dom (criticals f) ; :: thesis: f . (succ a) c= (criticals f) . (succ a)
(criticals f) . (succ a) is_a_fixpoint_of f by A5, Th29;
then ( (criticals f) . (succ a) in dom f & f . ((criticals f) . (succ a)) = (criticals f) . (succ a) ) ;
hence f . (succ a) c= (criticals f) . (succ a) by A1, A5, ORDINAL4:9, ORDINAL4:10; :: thesis: verum
end;
A6: for a being Ordinal st a <> 0 & a is limit_ordinal & ( for b being Ordinal st b in a holds
S1[b] ) holds
S1[a]
proof
let a be Ordinal; :: thesis: ( a <> 0 & a is limit_ordinal & ( for b being Ordinal st b in a holds
S1[b] ) implies S1[a] )
assume that
A7: ( a <> 0 & a is limit_ordinal ) and
A8: for b being Ordinal st b in a holds
S1[b] and
A9: a in dom (criticals f) ; :: thesis: f . a c= (criticals f) . a
( f . a is_limes_of f | a & (criticals f) . a is_limes_of (criticals f) | a ) by A1, A2, A7, A9, ORDINAL2:def 13;
then A10: ( f . a = lim (f | a) & (criticals f) . a = lim ((criticals f) | a) ) by ORDINAL2:def 10;
A11: ( f | a is increasing & (criticals f) | a is increasing ) by A1, ORDINAL4:15;
A12: ( a c= dom f & a c= dom (criticals f) ) by A2, A9, ORDINAL1:def 2;
then A13: ( dom (f | a) = a & dom ((criticals f) | a) = a ) by RELAT_1:62;
then ( Union (f | a) is_limes_of f | a & Union ((criticals f) | a) is_limes_of (criticals f) | a ) by A7, A11, ORDINAL5:6;
then A14: ( f . a = Union (f | a) & (criticals f) . a = Union ((criticals f) | a) ) by A10, ORDINAL2:def 10;
let b be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not b in f . a or b in (criticals f) . a )
assume b in f . a ; :: thesis: b in (criticals f) . a
then consider x being object such that
A15: ( x in a & b in (f | a) . x ) by A13, A14, CARD_5:2;
( (f | a) . x = f . x & ((criticals f) | a) . x = (criticals f) . x & f . x c= (criticals f) . x ) by A12, A8, A15, FUNCT_1:49;
hence b in (criticals f) . a by A15, A13, A14, CARD_5:2; :: thesis: verum
end;
thus for a being Ordinal holds S1[a] from ORDINAL2:sch 1(A3, A4, A6); :: thesis: verum