let n be Nat; :: thesis: for r being Real
for q being Point of (TOP-REAL n) st q = <*r*> holds
|.q.| = |.r.|
let r be Real; :: thesis: for q being Point of (TOP-REAL n) st q = <*r*> holds
|.q.| = |.r.|
let q be Point of (TOP-REAL n); :: thesis: ( q = <*r*> implies |.q.| = |.r.| )
assume A1: q = <*r*> ; :: thesis: |.q.| = |.r.|
reconsider rr = r as Element of REAL by XREAL_0:def 1;
reconsider xr = <*rr*> as Element of REAL 1 ;
reconsider qk = (q /. 1) ^2 as Element of REAL by XREAL_0:def 1;
len xr = 1 by FINSEQ_1:39;
then A2: q /. 1 = xr . 1 by A1, FINSEQ_4:15;
then ( len (sqr xr) = 1 & (sqr xr) . 1 = (q /. 1) ^2 ) by CARD_1:def 7, VALUED_1:11;
then A3: sqr xr = <*qk*> by FINSEQ_1:40;
sqrt ((q /. 1) ^2) = |.(q /. 1).| by COMPLEX1:72
.= |.r.| by A2 ;
then |.xr.| = |.rr.| by A3, FINSOP_1:11;
hence |.q.| = |.r.| by A1; :: thesis: verum