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