theorem Th33: :: FINSEQ_5:33

for n being Nat
for f being FinSequence holds rng (f /^ n) c= rng f