theorem Th3: :: NDIFF11:3

for m being non zero Nat
for s, s1 being FinSequence of REAL m
for s0 being Element of REAL m st s1 = s ^ <*s0*> holds
Sum s1 = (Sum s) + s0