for X being set
for f1, f2 being FinSequence of REAL st f2 = f1 * (Sgm X) & (dom f1) \ (f1 " {0}) c= X & X c= dom f1 holds
Sum f1 = Sum f2