theorem Th3: :: PDIFF_8:3

for n being non zero Element of NAT
for x being Point of (REAL-NS n)
for i being Nat st 1 <= i & i <= n holds
||.((Proj (i,n)) . x).|| <= ||.x.||