theorem Th4: :: INT_6:4

for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
for k being Nat st k <= len m1 holds
(m1 (#) m2) | k = (m1 | k) (#) (m2 | k)