theorem Th84: :: FINSEQ_6:84

for i, k being Nat
for D being non empty set
for f being FinSequence of D st i + k = len f holds
Rev (f /^ k) = (Rev f) | i