for f being complex-valued FinSequence st ex i being Nat st
( i in dom f & f . i = 0 ) holds
Product f = 0