let R be non degenerated Ring; :: thesis: for p being Polynomial of R holds min* { i where i is Nat : (- p) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R }
let p be Polynomial of R; :: thesis: min* { i where i is Nat : (- p) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R }

per cases ( p = 0_. R or p <> 0_. R ) ;

suppose p = 0_. R ; :: thesis: min* { i where i is Nat : (- p) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R }

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: verum

end;

suppose p <> 0_. R ; :: thesis: min* { i where i is Nat : (- p) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R }

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: not (- p) . j = 0. R

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

end;

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

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

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

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: for k being Nat st k in { i where i is Nat : (- p) . i <> 0. R } holds
j <= k

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

now :: thesis: ( p . i = 0. R implies (- p) . i = 0. R )

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

end;

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

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: verum

end;

end;