theorem Th25: :: NDIFF11:25

for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x holds
for s being FinSequence of REAL m
for t being FinSequence of REAL st dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) holds
(diff (f,x)) . (Sum s) = Sum t