( f is COMPLEX -valued & len f = 0 ) by Lm3;
hence Sum f is empty by Def9, BINOP_2:1; :: thesis: verum