theorem Th49: :: JORDAN1J:49

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