theorem Th4: :: PDIFF_8:4

for n being non zero Element of NAT
for x being Element of (REAL-NS n)
for i being Element of NAT holds ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).|