theorem Th5: :: MFOLD_1:5

for n being Nat
for p being Point of (TOP-REAL n) st n <> 0 & p is Point of (Tunit_ball n) holds
|.p.| < 1