theorem :: FINSEQ_6:132

for p being FinSequence
for m being Nat st 1 <= m & m <= len p holds
(m,m) -cut p = <*(p . m)*>