theorem :: AFINSQ_2:68

for cF being complex-valued XFinSequence
for c being Complex st rng cF c= {0,c} holds
Sum cF = c * (card (cF " {c}))