let
a
,
b
be
Element
of
F_Complex
;
:: thesis:
(
Im
a
=
0
&
Im
b
=
0
implies
Im
(
a
*
b
)
=
0
)
assume
(
Im
a
=
0
&
Im
b
=
0
) ;
:: thesis:
Im
(
a
*
b
)
=
0
hence
Im
(
a
*
b
)
=
(
Re
b
)
*
0
by
Th10
.=
0
;
:: thesis:
verum