theorem lemlowp1b: :: REALALG1:11

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