set
e
=
even_part
p
;
reconsider
z
=
0
as
Element
of
NAT
by
ORDINAL1:def 12
;
0
<=
degree
p
;
then
A1
:
p
.
z
<>
z
by
Def10
;
(
even_part
p
)
.
z
=
p
.
z
by
Def1
;
then
(
even_part
p
)
.
z
<>
0.
F_Complex
by
A1
,
COMPLFLD:def 1
;
hence
not
even_part
p
is
zero
by
FUNCOP_1:7
;
:: thesis:
verum