theorem :: RVSUM_1:103

for F being complex-valued FinSequence holds
( ex k being Nat st
( k in dom F & F . k = 0 ) iff Product F = 0 )