theorem Th22: :: FINSEQ_5:22

for i being Nat
for f, g being FinSequence st i <= len f holds
(f ^ g) | i = f | i