let n be Nat; :: thesis: for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
|.(p (/) |.p.|).| = 1
let p be Point of (TOP-REAL n); :: thesis: ( p <> 0. (TOP-REAL n) implies |.(p (/) |.p.|).| = 1 )
A1: |.p.| ^2 = Sum (sqr p) by TOPREAL9:5;
assume p <> 0. (TOP-REAL n) ; :: thesis: |.(p (/) |.p.|).| = 1
then |.p.| <> 0 by EUCLID_2:42;
then Sum ((sqr p) (/) (Sum (sqr p))) = 1 by A1, Th19;
hence |.(p (/) |.p.|).| = 1 by A1, Th18, SQUARE_1:18; :: thesis: verum