theorem :: FINSEQ_6:138

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