theorem Th61: :: NUMBER15:61

for n being Nat
for f being complex-valued FinSequence holds (f | n) " = (f ") | n