theorem Th7: :: FINSEQ_6:133

for p being FinSequence holds (1,(len p)) -cut p = p