for F being sequence of ExtREAL st ( for n being Element of NAT holds F . n = 0. ) holds
SUM F = 0.