let
x
be
Element
of
F_Complex
;
:: thesis:
(
Im
x
=
0
implies
x
=
x
*'
)
reconsider
d
=
x
as
Element
of
COMPLEX
by
COMPLFLD:def 1
;
assume
Im
x
=
0
;
:: thesis:
x
=
x
*'
hence
x
=
(
Re
d
)
+
(
(

(
Im
d
)
)
*
<i>
)
by
COMPLEX1:13
.=
x
*'
;
:: thesis:
verum