theorem :: FINSEQ_6:135

for p being FinSequence
for m being Nat st m <= len p holds
((1,m) -cut p) ^ (((m + 1),(len p)) -cut p) = p