let n be Element of NAT ; :: thesis: for r being Real
for q being Point of (TOP-REAL n) st q = <*r*> holds
|.q.| = abs r
let r be Real; :: thesis: for q being Point of (TOP-REAL n) st q = <*r*> holds
|.q.| = abs r
let q be Point of (TOP-REAL n); :: thesis: ( q = <*r*> implies |.q.| = abs r )
assume A1: q = <*r*> ; :: thesis: |.q.| = abs r
reconsider xr = <*r*> as Element of REAL 1 by FINSEQ_2:151;
len xr = 1 by FINSEQ_1:56;
then xr . 1 = xr /. 1 by FINSEQ_4:24;
then A2: q /. 1 = xr . 1 by A1;
then ( len (sqr xr) = 1 & (sqr xr) . 1 = (q /. 1) ^2 ) by FINSEQ_1:def 18, VALUED_1:11;
then A3: sqr xr = <*((q /. 1) ^2 )*> by FINSEQ_1:57;
sqrt ((q /. 1) ^2 ) = abs (q /. 1) by COMPLEX1:158
.= abs r by A2, FINSEQ_1:57 ;
hence |.q.| = abs r by A1, A3, FINSOP_1:12; :: thesis: verum