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