let L be non empty RelStr ; :: thesis: for f being sequence of the carrier of L

for n being Element of NAT holds { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L

let f be sequence of the carrier of L; :: thesis: for n being Element of NAT holds { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L

let n be Element of NAT ; :: thesis: { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L

set A = { (f . m) where m is Element of NAT : m <= n } ;

A1: { (f . m) where m is Element of NAT : m <= n } c= { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) }_{1}( set ) -> set = f . $1;

A5: { (f . m) where m is Element of NAT : m <= n } c= the carrier of L_{1}(m) where m is Element of NAT : m in {0} \/ (Seg n) } c= card ({0} \/ (Seg n))
from TREES_2:sch 2();

then A6: { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) } is finite ;

0 <= n by NAT_1:2;

then f . 0 in { (f . m) where m is Element of NAT : m <= n } ;

hence { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L by A1, A6, A5; :: thesis: verum

for n being Element of NAT holds { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L

let f be sequence of the carrier of L; :: thesis: for n being Element of NAT holds { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L

let n be Element of NAT ; :: thesis: { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L

set A = { (f . m) where m is Element of NAT : m <= n } ;

A1: { (f . m) where m is Element of NAT : m <= n } c= { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) }

proof

deffunc H
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (f . m) where m is Element of NAT : m <= n } or q in { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) } )

assume q in { (f . m) where m is Element of NAT : m <= n } ; :: thesis: q in { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) }

then consider m being Element of NAT such that

A2: q = f . m and

A3: m <= n ;

A4: ( m = 0 or m in Seg m ) by FINSEQ_1:3;

Seg m c= Seg n by A3, FINSEQ_1:5;

then ( m in {0} or m in Seg n ) by A4, TARSKI:def 1;

then m in {0} \/ (Seg n) by XBOOLE_0:def 3;

hence q in { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) } by A2; :: thesis: verum

end;assume q in { (f . m) where m is Element of NAT : m <= n } ; :: thesis: q in { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) }

then consider m being Element of NAT such that

A2: q = f . m and

A3: m <= n ;

A4: ( m = 0 or m in Seg m ) by FINSEQ_1:3;

Seg m c= Seg n by A3, FINSEQ_1:5;

then ( m in {0} or m in Seg n ) by A4, TARSKI:def 1;

then m in {0} \/ (Seg n) by XBOOLE_0:def 3;

hence q in { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) } by A2; :: thesis: verum

A5: { (f . m) where m is Element of NAT : m <= n } c= the carrier of L

proof

card { H
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (f . m) where m is Element of NAT : m <= n } or q in the carrier of L )

assume q in { (f . m) where m is Element of NAT : m <= n } ; :: thesis: q in the carrier of L

then ex m being Element of NAT st

( q = f . m & m <= n ) ;

hence q in the carrier of L ; :: thesis: verum

end;assume q in { (f . m) where m is Element of NAT : m <= n } ; :: thesis: q in the carrier of L

then ex m being Element of NAT st

( q = f . m & m <= n ) ;

hence q in the carrier of L ; :: thesis: verum

then A6: { (f . m) where m is Element of NAT : m in {0} \/ (Seg n) } is finite ;

0 <= n by NAT_1:2;

then f . 0 in { (f . m) where m is Element of NAT : m <= n } ;

hence { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L by A1, A6, A5; :: thesis: verum