let R be non degenerated Ring; :: thesis: for p, q being non zero Polynomial of R st 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 : q . i <> 0. R }
let p, q be non zero Polynomial of R; :: thesis: ( 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 : q . i <> 0. R } )
assume AS1: 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 : q . 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 Subset of NAT by TARSKI:def 3;
not min* cq in cp by AS1, NAT_1:def 1;
then p . (min* cq) = 0. R ;
then A: (p + q) . (min* cq) = (0. R) + (q . (min* cq)) by NORMSP_1:def 2;
min* cq in cq by NAT_1:def 1;
then consider u being Nat such that
H1: ( u = min* cq & q . u <> 0. R ) ;
B: min* cq in cpq by A, H1;
then reconsider cpq = cpq as non empty Subset of NAT ;

now :: thesis: for k being Nat st k in cpq holds
min* cq <= k

let k be Nat; :: thesis: ( k in cpq implies min* cq <= k )
assume k in cpq ; :: thesis: min* cq <= k
then consider v being Nat such that
H2: ( v = k & (p + q) . v <> 0. R ) ;

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

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

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

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

end;

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

assume p . j <> 0. R ; :: thesis: contradiction
then j in cp ;
then j >= min* cp by NAT_1:def 1;
hence contradiction by D0, AS1, XXREAL_0:2; :: thesis: verum

end;

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

end;

hence min* cq <= k by H2; :: thesis: verum

end;

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