theorem Th10: :: PETRI_DF:1

for x, y being Nat
for f being FinSequence st f /^ 1 is one-to-one & 1 < x & x <= len f & 1 < y & y <= len f & f . x = f . y holds
x = y