theorem LM89: :: DUALSP05:12

for A being non empty closed_interval Subset of REAL
for s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
for z being FinSequence of REAL
for g being Function of A,REAL
for t being Element of A st len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum z