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

|.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