theorem Th29: :: FINSEQ_3:31

for p being FinSequence
for x being object st x in rng p holds
1 in dom p