let l be limit_ordinal non empty Ordinal; :: thesis: for U being Universe st l in U & ( for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U
let U be Universe; :: thesis: ( l in U & ( for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) implies lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U )
set G = U -Veblen ;
assume that
A1: l in U and
A2: for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ; :: thesis: lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U
0 in l by ORDINAL3:8;
then omega c= l by ORDINAL1:def 11;
then A3: ( omega in U & l in On U ) by A1, CLASSES1:def 1, ORDINAL1:def 9;
then A4: ( (U -Veblen) . l = criticals ((U -Veblen) | l) & dom (U -Veblen) = On U ) by V;
l c= On U by A3, ORDINAL1:def 2;
then A5: dom ((U -Veblen) | l) = l by A4, RELAT_1:62;
set g = (U -Veblen) | l;

now

let a be ordinal number ; :: thesis: ( a in dom ((U -Veblen) | l) implies ((U -Veblen) | l) . a is Ordinal-Sequence of U )
assume A6: a in dom ((U -Veblen) | l) ; :: thesis: ((U -Veblen) | l) . a is Ordinal-Sequence of U
then ((U -Veblen) | l) . a = (U -Veblen) . a by A5, FUNCT_1:49;
hence ((U -Veblen) | l) . a is Ordinal-Sequence of U by A2, A5, A6; :: thesis: verum

end;

then reconsider f = lims ((U -Veblen) | l) as Ordinal-Sequence of U by A1, A5, ThL1;
((U -Veblen) | l) . 0 = (U -Veblen) . 0 by FUNCT_1:49, ORDINAL3:8;
then reconsider g0 = ((U -Veblen) | l) . 0 as Ordinal-Sequence of U by A2, ORDINAL3:8;
A8: dom f = On U by FUNCT_2:def 1;
deffunc H₁( set ) -> set = { ((((U -Veblen) | l) . b) . $1) where b is Element of dom ((U -Veblen) | l) : b in dom ((U -Veblen) | l) } ;
A7: f is non-decreasing

proof

let a be ordinal number ; :: according to ORDINAL5:def 2 :: thesis: for b₁ being set holds
( not a in b₁ or not b₁ in proj1 f or f . a c= f . b₁ )
let b be ordinal number ; :: thesis: ( not a in b or not b in proj1 f or f . a c= f . b )
assume B1: ( a in b & b in dom f ) ; :: thesis: f . a c= f . b
then a in dom f by ORDINAL1:10;
then B3: ( f . a = union H₁(a) & f . b = union H₁(b) ) by B1, LIM;
let c be ordinal number ; :: according to ORDINAL1:def 5 :: thesis: ( not c in f . a or c in f . b )
assume c in f . a ; :: thesis: c in f . b
then consider x being set such that
B4: ( c in x & x in H₁(a) ) by B3, TARSKI:def 4;
consider xa being Element of dom ((U -Veblen) | l) such that
B5: ( x = (((U -Veblen) | l) . xa) . a & xa in dom ((U -Veblen) | l) ) by B4;
((U -Veblen) | l) . xa = (U -Veblen) . xa by A5, FUNCT_1:49;
then reconsider h = ((U -Veblen) | l) . xa as increasing Ordinal-Sequence of U by A2, A5;
dom h = On U by FUNCT_2:def 1;
then h . a in h . b by A8, B1, ORDINAL2:def 12;
then h . a c= h . b by ORDINAL1:def 2;
then ( c in h . b & h . b in H₁(b) ) by B4, B5;
hence c in f . b by B3, TARSKI:def 4; :: thesis: verum

end;

f is continuous

proof

let a be ordinal number ; :: according to ORDINAL2:def 13 :: thesis: for b₁ being set holds
( not a in proj1 f or a = {} or not a is limit_ordinal or not b₁ = f . a or b₁ is_limes_of f | a )
let b be ordinal number ; :: thesis: ( not a in proj1 f or a = {} or not a is limit_ordinal or not b = f . a or b is_limes_of f | a )
assume C1: ( a in dom f & a <> {} & a is limit_ordinal & b = f . a ) ; :: thesis: b is_limes_of f | a
then C2: b = union H₁(a) by LIM;
D1: a c= dom f by C1, ORDINAL1:def 2;
then C3: dom (f | a) = a by RELAT_1:62;
C4: b = Union (f | a)

proof

thus b c= Union (f | a) :: according to XBOOLE_0:def 10 :: thesis: Union (f | a) c= b

proof

let c be ordinal number ; :: according to ORDINAL1:def 5 :: thesis: ( not c in b or c in Union (f | a) )
assume c in b ; :: thesis: c in Union (f | a)
then consider x being set such that
B4: ( c in x & x in H₁(a) ) by C2, TARSKI:def 4;
consider xa being Element of dom ((U -Veblen) | l) such that
B5: ( x = (((U -Veblen) | l) . xa) . a & xa in dom ((U -Veblen) | l) ) by B4;
((U -Veblen) | l) . xa = (U -Veblen) . xa by A5, FUNCT_1:49;
then reconsider h = ((U -Veblen) | l) . xa as normal Ordinal-Sequence of U by A2, A5;
C6: dom h = On U by FUNCT_2:def 1;
then C5: h . a is_limes_of h | a by A8, C1, ORDINAL2:def 13;
C7: h | a is increasing by ORDINAL4:15;
C8: dom (h | a) = a by A8, D1, C6, RELAT_1:62;
then Union (h | a) is_limes_of h | a by C1, C7, ORDINAL5:6;
then lim (h | a) = Union (h | a) by ORDINAL2:def 10;
then h . a = Union (h | a) by C5, ORDINAL2:def 10;
then consider y being set such that
C9: ( y in a & c in (h | a) . y ) by B4, B5, C8, CARD_5:2;
D3: y in On U by A8, C1, C9, ORDINAL1:10;
(h | a) . y = h . y by C9, FUNCT_1:49;
then (h | a) . y in H₁(y) by B5;
then c in union H₁(y) by C9, TARSKI:def 4;
then c in f . y by A8, D3, LIM;
then c in (f | a) . y by C9, FUNCT_1:49;
hence c in Union (f | a) by C3, C9, CARD_5:2; :: thesis: verum

end;

let c be ordinal number ; :: according to ORDINAL1:def 5 :: thesis: ( not c in Union (f | a) or c in b )
assume c in Union (f | a) ; :: thesis: c in b
then consider x being set such that
E1: ( x in dom (f | a) & c in (f | a) . x ) by CARD_5:2;
E2: (f | a) . x = f . x by C3, E1, FUNCT_1:49;
x in dom f by E1, RELAT_1:57;
then f . x = union H₁(x) by LIM;
then consider y being set such that
E4: ( c in y & y in H₁(x) ) by E1, E2, TARSKI:def 4;
consider z being Element of dom ((U -Veblen) | l) such that
E5: ( y = (((U -Veblen) | l) . z) . x & z in dom ((U -Veblen) | l) ) by E4;
((U -Veblen) | l) . z = (U -Veblen) . z by A5, FUNCT_1:49;
then reconsider h = ((U -Veblen) | l) . z as normal Ordinal-Sequence of U by A2, A5;
dom h = On U by FUNCT_2:def 1;
then h . x in h . a by E1, C3, C1, A8, ORDINAL2:def 12;
then h . x c= h . a by ORDINAL1:def 2;
then ( c in h . a & h . a in H₁(a) ) by E4, E5;
hence c in b by C2, TARSKI:def 4; :: thesis: verum

end;

f | a is non-decreasing by A7, ThND;
hence b is_limes_of f | a by C1, C3, C4, ORDINAL5:6; :: thesis: verum

end;

hence lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U by A7; :: thesis: verum