theorem Th113: :: FINSEQ_6:114

for D being non empty set
for n, m being Nat
for f being FinSequence of D st 1 <= m & m + n <= len f holds
(f /^ n) . m = f . (m + n)