theorem Th14: :: CARDFIN2:14

for X, N being XFinSequence of INT st len N = (len X) + 1 holds
for c being Integer st N | (len X) = c (#) X holds
Sum N = (c * (Sum X)) + (N . (len X))