theorem Th1: :: PDIFF_8:1

for n, i being Element of NAT
for q being Element of REAL n
for p being Point of (TOP-REAL n) st i in Seg n & q = p holds
|.(p /. i).| <= |.q.|