let R be non degenerated Ring; :: thesis: for p being non zero Polynomial of R holds { i where i is Nat : p . i <> 0. R } is non empty Subset of NAT
let p be non zero Polynomial of R; :: thesis: { i where i is Nat : p . i <> 0. R } is non empty Subset of NAT
A: 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
H: ( o = i & p . i <> 0. R ) ;
thus o in NAT by H, ORDINAL1:def 12; :: thesis: verum
end;
p <> 0_. R ;
hence { i where i is Nat : p . i <> 0. R } is non empty Subset of NAT by A, lemlp0, TARSKI:def 3; :: thesis: verum