theorem :: AFINSQ_2:52

for cF being complex-valued XFinSequence st cF = {} holds
Sum cF = 0 ;