theorem Th1: :: GRAPHSP:1

for p being FinSequence
for x being set holds
( ( not x in rng p & p is one-to-one ) iff p ^ <*x*> is one-to-one )