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:131;
len xr = 1 by FINSEQ_1:39;
then xr . 1 = xr /. 1 by FINSEQ_4:15;
then A2: q /. 1 = xr . 1 by A1;
then ( len (sqr xr) = 1 & (sqr xr) . 1 = (q /. 1) ^2 ) by CARD_1:def 7, VALUED_1:11;
then A3: sqr xr = <*((q /. 1) ^2)*> by FINSEQ_1:40;
sqrt ((q /. 1) ^2) = abs (q /. 1) by COMPLEX1:72
.= abs r by A2, FINSEQ_1:40 ;
hence |.q.| = abs r by A1, A3, FINSOP_1:11; :: thesis: verum