theorem Th16: :: PDIFF_8:16

for K being Real
for n being non zero Element of NAT
for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ) holds
||.s.|| <= n * K