reconsider
p1
=
p
,
q1
=
q
as
Polynomial
of
R
;
(
q
<>
0_.
R
&
p
<>
0_.
R
) ;
then
B
:
deg
(
p1
*'
q1
)
=
(
deg
p
)
+
(
deg
q
)
by
HURWITZ:23
;
deg
p
=
1
by
defl
;
hence
not
p
*'
q
is
linear
by
RATFUNC1:def 2
,
B
;
:: thesis:
verum