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 \/ (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 \/ (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 \/ (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 ;
then ( m in or m in Seg n ) by ;
then m in \/ (Seg n) by XBOOLE_0:def 3;
hence q in { (f . m) where m is Element of NAT : m in \/ (Seg n) } by A2; :: thesis: verum
end;
deffunc H1( 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 { H1(m) where m is Element of NAT : m in \/ (Seg n) } c= card ( \/ (Seg n)) from then A6: { (f . m) where m is Element of NAT : m in \/ (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