let r be real number ; :: thesis: |.<*r*>.| = abs r
set f = <*r*>;
sqr <*r*> = <*(r ^2)*> by RVSUM_1:55;
then Sum (sqr <*r*>) = r ^2 by RVSUM_1:73;
hence |.<*r*>.| = abs r by COMPLEX1:72; :: thesis: verum