for D being finite set
for n being Element of NAT
for X being set st X = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } holds
X is finite