theorem Th51: :: FINSEQ_4:51

for p being FinSequence
for x being object st x in rng p holds
p = ((p -| x) ^ <*x*>) ^ (p |-- x)