reconsider
b
=
x
"
as
Element
of
F_Real
by
XREAL_0:def 1
;
A1
:
a
<>
0.
F_Real
;
assume
x
=
a
;
:: thesis:
a
"
=
x
"
then
b
*
a
=
1.
F_Real
by
A1
,
XCMPLX_0:def 7
;
hence
a
"
=
x
"
by
A1
,
Def10
;
:: thesis:
verum