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