theorem EMP: :: FINSEQ_9:1

for f being complex-valued FinSequence holds 0 (#) f = (len f) |-> 0