let R be non degenerated Ring; :: thesis:
let p be Polynomial of R; :: thesis:

per cases ;

suppose p = 0_. R ; :: thesis:

then - p = p by HURWITZ:9;
hence min* { i where i is Nat : (- p) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R } ; :: thesis:

end;

suppose p <> 0_. R ; :: thesis:

then reconsider pp = p as non zero Polynomial of R by UPROOTS:def 5;
reconsider cp = { i where i is Nat : pp . i <> 0. R } as non empty Subset of NAT by lemlp1;
min* cp in cp by NAT_1:def 1;
then consider j being Nat such that
A0: ( j = min* cp & p . j <> 0. R ) ;

now :: thesis:

assume (- p) . j = 0. R ; :: thesis:
then A1: 0. R = - (p . j) by BHSP_1:44;
p . j = - (- (p . j))
.= 0. R by A1 ;
hence contradiction by A0; :: thesis:

end;

then A: j in { i where i is Nat : (- p) . i <> 0. R } ;

now :: thesis:

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

end;

then reconsider cmp = { i where i is Nat : (- p) . i <> 0. R } as non empty Subset of NAT by A, TARSKI:def 3;

now :: thesis:

let k be Nat; :: thesis:
assume k in { i where i is Nat : (- p) . i <> 0. R } ; :: thesis:
then consider i being Nat such that
A3: ( k = i & (- p) . i <> 0. R ) ;

now :: thesis:

assume p . i = 0. R ; :: thesis:
then - (p . i) = 0. R ;
hence (- p) . i = 0. R by BHSP_1:44; :: thesis:

end;

then i in cp by A3;
hence j <= k by A3, A0, NAT_1:def 1; :: thesis:

end;

then j = min* cmp by A, NAT_1:def 1;
hence min* { i where i is Nat : (- p) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R } by A0; :: thesis:

end;

end;