theorem Th4: :: INTEGR20:4

for X being RealNormSpace
for n, m being Nat
for a being Function of [:(Seg n),(Seg m):],X
for p, q being FinSequence of X st dom p = Seg n & ( for i being Nat st i in dom p holds
ex r being FinSequence of X st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . (i,j) ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of X st
( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ) holds
Sum p = Sum q