for p being FinSequence
for x being object st x in rng p holds
( 1 <= x .. p & x .. p <= len p )