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