let
z
be
Element
of
F_Complex
;
:: thesis:
z
*
(
z
*'
)
=
|.
z
.|
^2
reconsider
a
=
z
as
Element
of
COMPLEX
by
COMPLFLD:def 1
;
thus
z
*
(
z
*'
)
=
(
|.
a
.|
^2
)
+
(
0
*
<i>
)
by
Th4
.=
|.
z
.|
^2
;
:: thesis:
verum