let U be Universe; :: thesis: for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & dom g in U & ( for a being ordinal number st a in dom g holds
g . a is Ordinal-Sequence of U ) holds
lims g is Ordinal-Sequence of U
let g be Ordinal-Sequence-valued T-Sequence; :: thesis: ( dom g <> {} & dom g in U & ( for a being ordinal number st a in dom g holds
g . a is Ordinal-Sequence of U ) implies lims g is Ordinal-Sequence of U )
assume Z0: ( dom g <> {} & dom g in U ) ; :: thesis: ( ex a being ordinal number st
( a in dom g & g . a is not Ordinal-Sequence of U ) or lims g is Ordinal-Sequence of U )
assume Z1: for a being ordinal number st a in dom g holds
g . a is Ordinal-Sequence of U ; :: thesis: lims g is Ordinal-Sequence of U
reconsider g0 = g . 0 as Ordinal-Sequence of U by Z1, Z0, ORDINAL3:8;
Z2: dom (lims g) = dom g0 by LIM
.= On U by FUNCT_2:def 1 ;
rng (lims g) c= On U

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (lims g) or x in On U )
assume x in rng (lims g) ; :: thesis: x in On U
then consider y being set such that
A1: ( y in dom (lims g) & x = (lims g) . y ) by FUNCT_1:def 3;
reconsider y = y as Ordinal by A1;
set X = { ((g . b) . y) where b is Element of dom g : b in dom g } ;
A2: x = union { ((g . b) . y) where b is Element of dom g : b in dom g } by A1, LIM;
reconsider a = dom g as non empty Ordinal of U by Z0;
deffunc H₁( set ) -> set = (g . $1) . y;
A3: card { H₁(b) where b is Element of a : b in a } c= card a from TREES_2:sch 2();
card a c= a by CARD_1:8;
then card { ((g . b) . y) where b is Element of dom g : b in dom g } c= a by A3, XBOOLE_1:1;
then card { ((g . b) . y) where b is Element of dom g : b in dom g } in U by CLASSES1:def 1;
then card { ((g . b) . y) where b is Element of dom g : b in dom g } in On U by ORDINAL1:def 9;
then C4: card { ((g . b) . y) where b is Element of dom g : b in dom g } in card U by CLASSES2:9;
C5: { ((g . b) . y) where b is Element of dom g : b in dom g } c= On U

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { ((g . b) . y) where b is Element of dom g : b in dom g } or z in On U )
assume z in { ((g . b) . y) where b is Element of dom g : b in dom g } ; :: thesis: z in On U
then consider b being Element of a such that
C6: ( z = (g . b) . y & b in a ) ;
reconsider f = g . b as Ordinal-Sequence of U by Z1;
z = f . y by C6;
hence z in On U by ORDINAL1:def 9; :: thesis: verum

end;

then reconsider u = union { ((g . b) . y) where b is Element of dom g : b in dom g } as Ordinal by ORDINAL3:4;
On U c= U by ORDINAL2:7;
then { ((g . b) . y) where b is Element of dom g : b in dom g } c= U by C5, XBOOLE_1:1;
then { ((g . b) . y) where b is Element of dom g : b in dom g } in U by C4, CLASSES1:1;
then u in U by CLASSES2:59;
hence x in On U by A2, ORDINAL1:def 9; :: thesis: verum

end;

hence lims g is Ordinal-Sequence of U by Z2, FUNCT_2:2; :: thesis: verum