theorem Th22: :: FINSEQ_5:22

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