theorem Th3: :: INTEGR23:3

for p, 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