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