let R be non degenerated Ring; :: thesis: 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 } ))
let p, q be non zero Polynomial of R; :: thesis: ( (p . (min* { i where i is Nat : p . i <> 0. R } )) + (q . (min* { i where i is Nat : q . i <> 0. R } )) <> 0. R implies 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 } )) )
assume XX: (p . (min* { i where i is Nat : p . i <> 0. R } )) + (q . (min* { i where i is Nat : q . i <> 0. R } )) <> 0. R ; :: thesis: 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 } ))
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;

per cases ( min* cp > min* cq or min* cp < min* cq or min* cp = min* cq ) by XXREAL_0:1;

suppose A: min* cp > min* cq ; :: thesis: 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 } ))

then min* cpq = min* cq by lemlowp1a1;
hence 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 } )) by A, XXREAL_0:def 9; :: thesis: verum

end;

suppose A: min* cp < min* cq ; :: thesis: 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 } ))

then min* cpq = min* cp by lemlowp1a1;
hence 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 } )) by A, XXREAL_0:def 9; :: thesis: verum

end;

suppose A: min* cp = min* cq ; :: thesis: 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 } ))

then (p + q) . (min* cp) <> 0. R by XX, NORMSP_1:def 2;
then D1: min* cp in cpq ;
then p + q <> 0_. R by lemlp0;
then D4: min* cpq >= min* cp by A, lemlowp1a2;
not min* cpq > min* cp by D1, NAT_1:def 1;
hence 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 } )) by A, D4, XXREAL_0:1; :: thesis: verum

end;

end;