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