theorem Th10: :: INTEGR20:10

for Y being RealNormSpace
for p being FinSequence of Y
for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds
||.(p /. j).|| <= q . j ) holds
||.(Sum p).|| <= Sum q