theorem Th15: :: PDIFF_8:15

for K being Real
for n being Nat
for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds
|.(s . i).| <= K ) holds
|.s.| <= n * K