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