theorem lemlowp3b: :: REALALG1:13

for R being domRing
for p, q being non zero Polynomial of 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 } )