theorem Th5: :: INT_6:5

for f being complex-valued FinSequence
for i being Nat st i + 1 <= len f holds
(f | i) ^ <*(f . (i + 1))*> = f | (i + 1)