theorem Th33: :: FINSEQ_5:33

for n being Nat
for D being non empty set
for f being FinSequence of D holds rng (f /^ n) c= rng f