theorem :: FINSEQ_6:136

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