theorem Th56: :: FINSEQ_4:56

for p being FinSequence
for x being object st x in rng p & p - {x} is one-to-one & p - {x} = (p -| x) ^ (p |-- x) holds
p is one-to-one