theorem lemlowp3a: :: REALALG1:12

for R being non degenerated Ring
for p, q being non zero Polynomial of R st p *' q <> 0_. R holds
min* { i where i is Nat : (p *' q) . i <> 0. R } >= (min* { i where i is Nat : p . i <> 0. R } ) + (min* { i where i is Nat : q . i <> 0. R } )