let L be non empty RelStr ; :: thesis: for f being Function of NAT ,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 Function of NAT ,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 } ;
0 <= n by NAT_1:2;
then A1: f . 0 in { (f . m) where m is Element of NAT : m <= n } ;
A2: { (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 set ; :: 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
A3: q = f . m and
A4: m <= n ;
A5: Seg m c= Seg n by A4, FINSEQ_1:7;
( m = 0 or m in Seg m ) by FINSEQ_1:5;
then ( m in {0 } or m in Seg n ) by A5, 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 A3; :: thesis: verum

end;

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

proof

let q be set ; :: 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 consider m being Element of NAT such that
A7: q = f . m and
m <= n ;
thus q in the carrier of L by A7; :: thesis: verum

end;

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