theorem Th81: :: FINSEQ_6:81

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