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