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