let
x
,
a
be
Real
;
:: thesis:
(
a
<>
0
&
Polynom
(
a
,
0
,
0
,
x
)
=
0
implies
x
=
0
)
assume
that
A1
:
a
<>
0
and
A2
:
Polynom
(
a
,
0
,
0
,
x
)
=
0
;
:: thesis:
x
=
0
(
(
a
*
(
x
^2
)
)
+
(
0
*
x
)
)
+
0
=
0
by
A2
,
POLYEQ_1:def 2
;
then
x
^2
=
0
by
A1
;
hence
x
=
0
;
:: thesis:
verum