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

A: now :: thesis: for i being Nat holds p . i = 0. R

let i be Nat; :: thesis: p . i = 0. R
thus p . i = (p . i) * (1. R)
.= (p . i) * (0. R) by STRUCT_0:def 8
.= 0. R ; :: thesis: verum

end;

set M = { i where i is Nat : p . i <> 0. R } ;

now :: thesis: ( { i where i is Nat : p . i <> 0. R } <> {} implies for x being Element of { i where i is Nat : p . i <> 0. R } holds contradiction )

assume B: { i where i is Nat : p . i <> 0. R } <> {} ; :: thesis: for x being Element of { x where i is Nat : p . x <> 0. R } holds contradiction
let x be Element of { i where i is Nat : p . i <> 0. R } ; :: thesis: contradiction
x in { i where i is Nat : p . i <> 0. R } by B;
then consider j being Nat such that
H1: ( j = x & p . j <> 0. R ) ;
thus contradiction by H1, A; :: thesis: verum

end;

hence { i where i is Nat : p . i <> 0. R } = {} ; :: thesis: verum