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