let R be Ring; :: thesis: for p being Polynomial of R holds min* { i where i is Nat : (p + (0_. R)) . 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 + (0_. R)) . i <> 0. R } = min* { 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 cp = { i where i is Nat : p . i <> 0. R } as Subset of NAT by TARSKI:def 3;

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

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

end;

then reconsider cpq = { i where i is Nat : (p + (0_. R)) . i <> 0. R } as Subset of NAT by TARSKI:def 3;

per cases ( not cp is empty or cp is empty ) ;

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

then min* cp in cp by NAT_1:def 1;
then consider i being Nat such that
H1: ( min* cp = i & p . i <> 0. R ) ;
(p + (0_. R)) . i = (p . i) + ((0_. R) . i) by NORMSP_1:def 2
.= (p . i) + (0. R) by ORDINAL1:def 12, FUNCOP_1:7
.= p . i ;
then B: min* cp in cpq by H1;

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

let k be Nat; :: thesis: ( k in cpq implies min* cp <= k )
assume k in cpq ; :: thesis: min* cp <= k
then consider i being Nat such that
C1: ( k = i & (p + (0_. R)) . i <> 0. R ) ;

now :: thesis: not min* cp > k

assume min* cp > k ; :: thesis: contradiction
then C2: not k in cp by NAT_1:def 1;
(p + (0_. R)) . k = (p . k) + ((0_. R) . k) by NORMSP_1:def 2
.= (p . k) + (0. R) by ORDINAL1:def 12, FUNCOP_1:7
.= 0. R by C2 ;
hence contradiction by C1; :: thesis: verum

end;

hence min* cp <= k ; :: thesis: verum

end;

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

end;

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

then p = 0_. R by lemlp0;
hence min* { i where i is Nat : (p + (0_. R)) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R } by A, lemlp0, POLYNOM3:28; :: thesis: verum

end;

end;