let r be Real; :: thesis: |.|[r]|.| = |.r.|
set p = |[r]|;
reconsider w = |[r]| as Element of REAL 1 by EUCLID:22;
reconsider r2 = r ^2 as Element of REAL by XREAL_0:def 1;
sqr w = <*r2*> by RVSUM_1:55;
then |.|[r]|.| = sqrt r2 by FINSOP_1:11
.= |.r.| by COMPLEX1:72 ;
hence |.|[r]|.| = |.r.| ; :: thesis: verum