theorem :: PDIFF_8:5

for n being non zero Element of NAT
for x being Element of REAL n
for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . x).| <= |.x.|