theorem Th13: :: POLYFORM:15

for a, b, s being complex-valued FinSequence st len s > 0 & len a = len s & len b = len s & ( for n being Nat st 1 <= n & n <= len s holds
s . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len s holds
b . k = - (a . (k + 1)) ) holds
Sum s = (a . 1) + (b . (len s))