theorem FINSEQ681: :: NEWTON04:35

for f being FinSequence
for a, b being Nat holds (f /^ a) /^ b = f /^ (a + b)