theorem Th9: :: CQC_SIM1:9

for l being FinSequence holds rng l = { (l . i) where i is Nat : ( 1 <= i & i <= len l ) }