theorem Th24: :: PDIFF_7:24

for m being non zero Nat
for v, w, u being FinSequence of REAL m st dom v = dom w & u = v + w holds
Sum u = (Sum v) + (Sum w)