theorem Th14: :: FINSEQ_6:14

for f1, f2 being FinSequence
for i being Nat holds (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i))