let F be Ordinal-Sequence-valued T-Sequence; :: thesis: ( dom F <> {} & ( for a being ordinal number st a in dom F holds
F . a is normal ) implies for a being ordinal number
for f being Ordinal-Sequence st a in dom (criticals F) & f in rng F holds
f . a c= (criticals F) . a )
assume that
X0: dom F <> {} and
X1: for a being ordinal number st a in dom F holds
F . a is normal ; :: thesis: for a being ordinal number
for f being Ordinal-Sequence st a in dom (criticals F) & f in rng F holds
f . a c= (criticals F) . a
let a be ordinal number ; :: thesis: for f being Ordinal-Sequence st a in dom (criticals F) & f in rng F holds
f . a c= (criticals F) . a
let f be Ordinal-Sequence; :: thesis: ( a in dom (criticals F) & f in rng F implies f . a c= (criticals F) . a )
assume that
X2: a in dom (criticals F) and
X3: f in rng F ; :: thesis: f . a c= (criticals F) . a
consider x being set such that
A0: ( x in dom F & f = F . x ) by X3, FUNCT_1:def 3;
A1: f is normal by A0, X1;
set g = criticals F;
A2: dom (criticals F) c= dom f by X3, ThA5;
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 A0, ThA2;
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 A0, C2, ThA2;
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
criticals F is continuous by X0, X1, ThAA;
then ( 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;

for a being ordinal number holds S₁[a] from ORDINAL2:sch 1(00, 01, 02);
hence f . a c= (criticals F) . a by X2; :: thesis: verum