theorem Th17: :: PDIFF_6:17

for m being Nat
for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Nat st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq