let F be Ordinal-Sequence-valued Sequence; :: thesis: ( dom F <> {} & ( for a being Ordinal st a in dom F holds
F . a is normal ) implies for a being Ordinal
for f being Ordinal-Sequence st a in dom (criticals F) & f in rng F holds
f . a c= (criticals F) . a )
assume that
A1: dom F <> {} and
A2: for a being Ordinal st a in dom F holds
F . a is normal ; :: thesis: for a being Ordinal
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; :: 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
A3: a in dom (criticals F) and
A4: f in rng F ; :: thesis: f . a c= (criticals F) . a
consider x being object such that
A5: ( x in dom F & f = F . x ) by A4, FUNCT_1:def 3;
A6: f is normal by A5, A2;
set g = criticals F;
A7: dom (criticals F) c= dom f by A4, Th49;
defpred S1[ Ordinal] means ( $1 in dom (criticals F) implies f . $1 c= (criticals F) . $1 );
A8: 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 A5, Th47;
then ( f . ((criticals F) . 0) = (criticals F) . 0 & (criticals F) . 0 in dom f ) ;
hence f . 0 c= (criticals F) . 0 by A6, ORDINAL4:9, XBOOLE_1:2; :: thesis: verum
end;
A9: 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
A10: 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, A10, Th47;
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 A6, A10, ORDINAL4:9, ORDINAL4:10; :: thesis: verum
end;
A11: 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
A12: ( a <> 0 & a is limit_ordinal ) and
A13: for b being Ordinal st b in a holds
S1[b] and
A14: a in dom (criticals F) ; :: thesis: f . a c= (criticals F) . a
criticals F is continuous by A1, A2, Th53;
then ( f . a is_limes_of f | a & (criticals F) . a is_limes_of (criticals F) | a ) by A6, A7, A12, A14, ORDINAL2:def 13;
then A15: ( f . a = lim (f | a) & (criticals F) . a = lim ((criticals F) | a) ) by ORDINAL2:def 10;
A16: ( f | a is increasing & (criticals F) | a is increasing ) by A6, ORDINAL4:15;
A17: ( a c= dom f & a c= dom (criticals F) ) by A7, A14, ORDINAL1:def 2;
then A18: ( 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 A12, A16, ORDINAL5:6;
then A19: ( f . a = Union (f | a) & (criticals F) . a = Union ((criticals F) | a) ) by A15, 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
A20: ( x in a & b in (f | a) . x ) by A18, A19, CARD_5:2;
( (f | a) . x = f . x & ((criticals F) | a) . x = (criticals F) . x & f . x c= (criticals F) . x ) by A17, A13, A20, FUNCT_1:49;
hence b in (criticals F) . a by A20, A18, A19, CARD_5:2; :: thesis: verum
end;
for a being Ordinal holds S1[a] from ORDINAL2:sch 1(A8, A9, A11);
 hence f . a c= (criticals F) . a by A3; :: thesis: verum