let n be Nat; :: thesis: for p being Point of (TOP-REAL n) st n <> 0 & p is Point of (Tunit_ball n) holds
|.p.| < 1
let p be Point of (TOP-REAL n); :: thesis: ( n <> 0 & p is Point of (Tunit_ball n) implies |.p.| < 1 )
reconsider j = 1 as Real ;
assume n <> 0 ; :: thesis: ( not p is Point of (Tunit_ball n) or |.p.| < 1 )
then reconsider n1 = n as non zero Element of NAT by ORDINAL1:def 12;
assume p is Point of (Tunit_ball n) ; :: thesis: |.p.| < 1
then p in the carrier of (Tball ((0. (TOP-REAL n1)),j)) ;
then p in Ball ((0. (TOP-REAL n1)),1) by MFOLD_0:2;
hence |.p.| < 1 by TOPREAL9:10; :: thesis: verum