let R be non degenerated Ring; :: thesis: for p, q being non zero Polynomial of R st p + q <> 0_. R & min* { i where i is Nat : p . i <> 0. R } = min* { i where i is Nat : q . i <> 0. R } holds
min* { i where i is Nat : (p + q) . i <> 0. R } >= min* { i where i is Nat : p . i <> 0. R }
let p, q be non zero Polynomial of R; :: thesis: ( p + q <> 0_. R & min* { i where i is Nat : p . i <> 0. R } = min* { i where i is Nat : q . i <> 0. R } implies min* { i where i is Nat : (p + q) . i <> 0. R } >= min* { i where i is Nat : p . i <> 0. R } )
assume XX: ( p + q <> 0_. R & min* { i where i is Nat : p . i <> 0. R } = min* { i where i is Nat : q . i <> 0. R } ) ; :: thesis: min* { i where i is Nat : (p + q) . i <> 0. R } >= min* { i where i is Nat : p . i <> 0. R }
reconsider cp = { i where i is Nat : p . i <> 0. R } , cq = { i where i is Nat : q . i <> 0. R } as non empty Subset of NAT by lemlp1;

now :: thesis: for o being object st o in { i where i is Nat : (p + q) . i <> 0. R } holds
o in NAT

let o be object ; :: thesis: ( o in { i where i is Nat : (p + q) . i <> 0. R } implies o in NAT )
assume o in { i where i is Nat : (p + q) . i <> 0. R } ; :: thesis: o in NAT
then consider i being Nat such that
H1: ( o = i & (p + q) . i <> 0. R ) ;
thus o in NAT by H1, ORDINAL1:def 12; :: thesis: verum

end;

then reconsider cpq = { i where i is Nat : (p + q) . i <> 0. R } as non empty Subset of NAT by lemlp0, XX, TARSKI:def 3;
min* cpq in cpq by NAT_1:def 1;
then consider u being Nat such that
H1: ( u = min* cpq & (p + q) . u <> 0. R ) ;

now :: thesis: for j being Nat st j < min* cp holds
(p + q) . j = 0. R

let j be Nat; :: thesis: ( j < min* cp implies (p + q) . j = 0. R )
assume D0: j < min* cp ; :: thesis: (p + q) . j = 0. R

D1a: now :: thesis: not p . j <> 0. R

assume p . j <> 0. R ; :: thesis: contradiction
then j in cp ;
hence contradiction by D0, NAT_1:def 1; :: thesis: verum

end;

now :: thesis: not q . j <> 0. R

assume q . j <> 0. R ; :: thesis: contradiction
then j in cq ;
hence contradiction by XX, D0, NAT_1:def 1; :: thesis: verum

end;

hence (p + q) . j = (p . j) + (0. R) by NORMSP_1:def 2
.= 0. R by D1a ;
:: thesis: verum

end;

hence min* { i where i is Nat : (p + q) . i <> 0. R } >= min* { i where i is Nat : p . i <> 0. R } by H1; :: thesis: verum