let U be Universe; :: thesis: for g being Ordinal-Sequence-valued Sequence st dom g <> {} & dom g in U & ( for a being Ordinal 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 Sequence; :: thesis: ( dom g <> {} & dom g in U & ( for a being Ordinal st a in dom g holds
g . a is Ordinal-Sequence of U ) implies lims g is Ordinal-Sequence of U )
assume A1: ( dom g <> {} & dom g in U ) ; :: thesis: ( ex a being Ordinal st
( a in dom g & g . a is not Ordinal-Sequence of U ) or lims g is Ordinal-Sequence of U )
assume A2: for a being Ordinal 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 A2, A1, ORDINAL3:8;
A3: dom (lims g) = dom g0 by Def12
.= On U by FUNCT_2:def 1 ;
rng (lims g) c= On U

proof

let x be object ; :: 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 object such that
A4: ( y in dom (lims g) & x = (lims g) . y ) by FUNCT_1:def 3;
reconsider y = y as Ordinal by A4;
set X = { ((g . b) . y) where b is Element of dom g : b in dom g } ;
A5: x = union { ((g . b) . y) where b is Element of dom g : b in dom g } by A4, Def12;
reconsider a = dom g as non empty Ordinal of U by A1;
deffunc H₁( set ) -> set = (g . $1) . y;
A6: 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 A6;
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 A7: card { ((g . b) . y) where b is Element of dom g : b in dom g } in card U by CLASSES2:9;
A8: { ((g . b) . y) where b is Element of dom g : b in dom g } c= On U

proof

let z be object ; :: 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
A9: ( z = (g . b) . y & b in a ) ;
reconsider f = g . b as Ordinal-Sequence of U by A2;
z = f . y by A9;
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 A8;
then { ((g . b) . y) where b is Element of dom g : b in dom g } in U by A7, CLASSES1:1;
then u in U by CLASSES2:59;
hence x in On U by A5, ORDINAL1:def 9; :: thesis: verum

end;

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