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 ;
len xr = 1 by FINSEQ_1:56;
then xr . 1 = xr /. 1 by FINSEQ_4:24;
then A2: Proj q,1 = xr . 1 by A1, JORDAN2B:def 1;
A3: len (sqr xr) = 1 by FINSEQ_1:def 18;
(sqr xr) . 1 = (Proj q,1) ^2 by A2, VALUED_1:11;
then A4: sqr xr = <*((Proj q,1) ^2 )*> by A3, FINSEQ_1:57;
sqrt ((Proj q,1) ^2 ) = abs (Proj q,1) by COMPLEX1:158
.= abs r by A2, FINSEQ_1:57 ;
hence |.q.| = abs r by A1, A4, FINSOP_1:12; :: thesis: verum