theorem Th8: :: FINSEQ_2:10

for b being object
for p being FinSequence st b in rng p holds
ex i being Nat st
( i in dom p & p . i = b )