theorem Th9: :: INTEGR20:9

for Y being RealNormSpace
for xseq being FinSequence of Y
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Point of Y st
( v = xseq /. i & yseq . i = ||.v.|| ) ) holds
||.(Sum xseq).|| <= Sum yseq