per cases ( p = 0_. R or q = 0_. R or ( p <> 0_. R & q <> 0_. R ) ) ;

suppose ( p = 0_. R or q = 0_. R ) ; :: thesis: p *' q is constant

hence p *' q is constant ; :: thesis: verum

end;

suppose A: ( p <> 0_. R & q <> 0_. R ) ; :: thesis: p *' q is constant

then ( deg p >= 0 & deg q >= 0 ) by T8;
then B: ( deg p = 0 & deg q = 0 ) by RATFUNC1:def 2;
deg (p *' q) = (deg p) + (deg q) by A, HURWITZ:23;
hence p *' q is constant by B, RATFUNC1:def 2; :: thesis: verum

end;

end;