theorem Th3: :: AFINSQ_2:3

for x being object
for p being XFinSequence st x in rng p holds
ex i being Element of NAT st
( i in dom p & p . i = x )