theorem FINSEQ165: :: NEWTON07:48

for n being non zero Nat
for f, g being FinSequence holds (f ^ g) . ((len f) + n) = g . n