:: deftheorem Def1 defines +...+ FLEXARY1:def 1 :
for k, n being Nat
for f, g being complex-valued Function
for b₅ being complex number holds
( ( f = g & k <= n implies ( b₅ = (f,k) +...+ (g,n) iff for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
b₅ = Sum (h | ((n -' k) + 1)) ) ) & ( ( not f = g or not k <= n ) implies ( b₅ = (f,k) +...+ (g,n) iff b₅ = 0 ) ) );