theorem Th17: :: TOPREALC:17

for i, n being Nat
for c being Complex
for g1 being b₂ -element complex-valued FinSequence holds (g1 +* (i,c)) - g1 = (0* n) +* (i,(c - (g1 . i)))