theorem Th36: :: FINSEQ_5:36

for i being Nat
for f, g being FinSequence holds (f ^ g) /^ ((len f) + i) = g /^ i