let f be Ordinal-Sequence; :: thesis: ( f is normal implies for a being ordinal number st a in dom (criticals f) holds
f . a c= (criticals f) . a )
assume A1: f is normal ; :: thesis: for a being ordinal number 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 Th05;
defpred S₁[ Ordinal] means ( $1 in dom (criticals f) implies f . $1 c= (criticals f) . $1 );
00: S₁[ {} ]

proof

assume {} in dom (criticals f) ; :: thesis: f . {} c= (criticals f) . {}
then (criticals f) . 0 is_a_fixpoint_of f by Th02;
then ( f . ((criticals f) . 0) = (criticals f) . 0 & (criticals f) . 0 in dom f ) by ABIAN:def 3;
hence f . {} c= (criticals f) . {} by A1, ORDINAL4:9, XBOOLE_1:2; :: thesis: verum

end;

01: for a being ordinal number st S₁[a] holds
S₁[ succ a]

proof

let a be ordinal number ; :: thesis: ( S₁[a] implies S₁[ succ a] )
assume that
S₁[a] and
C2: 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 C2, Th02;
then ( (criticals f) . (succ a) in dom f & f . ((criticals f) . (succ a)) = (criticals f) . (succ a) ) by ABIAN:def 3;
hence f . (succ a) c= (criticals f) . (succ a) by A1, C2, ORDINAL4:9, ORDINAL4:10; :: thesis: verum

end;

02: for a being ordinal number st a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S₁[b] ) holds
S₁[a]

proof

let a be ordinal number ; :: thesis: ( a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S₁[b] ) implies S₁[a] )
assume that
Z1: ( a <> {} & a is limit_ordinal ) and
Z2: for b being ordinal number st b in a holds
S₁[b] and
Z3: 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, Z1, Z3, ORDINAL2:def 13;
then Z4: ( f . a = lim (f | a) & (criticals f) . a = lim ((criticals f) | a) ) by ORDINAL2:def 10;
Z5: ( f | a is increasing & (criticals f) | a is increasing ) by A1, ORDINAL4:15;
Z9: ( a c= dom f & a c= dom (criticals f) ) by A2, Z3, ORDINAL1:def 2;
then Z7: ( 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 Z1, Z5, ORDINAL5:6;
then Z6: ( f . a = Union (f | a) & (criticals f) . a = Union ((criticals f) | a) ) by Z4, ORDINAL2:def 10;
let b be ordinal number ; :: 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 set such that
Z8: ( x in a & b in (f | a) . x ) by Z7, Z6, CARD_5:2;
( (f | a) . x = f . x & ((criticals f) | a) . x = (criticals f) . x & f . x c= (criticals f) . x ) by Z9, Z2, Z8, FUNCT_1:49;
hence b in (criticals f) . a by Z8, Z7, Z6, CARD_5:2; :: thesis: verum

end;

thus for a being ordinal number holds S₁[a] from ORDINAL2:sch 1(00, 01, 02); :: thesis: verum