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) }

proof

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;

deffunc H₁( set ) -> set = f . $1;
A5: { (f . m) where m is Element of NAT : m <= n } c= the carrier of L

proof

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;

card { H₁(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