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