theorem Th22: :: FINSEQ_4:22

for p being FinSequence
for x being object st x in rng p holds
( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT )