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 S₁[ Ordinal] means ( $1 in dom (criticals f) implies f . $1 c= (criticals f) . $1 );
A3: S₁[ 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 S₁[a] holds
S₁[ succ a]

proof

let a be Ordinal; :: thesis: ( S₁[a] implies S₁[ succ a] )
assume that
S₁[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
S₁[b] ) holds
S₁[a]

proof

let a be Ordinal; :: thesis: ( a <> 0 & a is limit_ordinal & ( for b being Ordinal st b in a holds
S₁[b] ) implies S₁[a] )
assume that
A7: ( a <> 0 & a is limit_ordinal ) and
A8: for b being Ordinal st b in a holds
S₁[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 S₁[a] from ORDINAL2:sch 1(A3, A4, A6); :: thesis: verum