let R be Ring; :: thesis: for p being Polynomial of R
for n being Nat holds p <> n
let p be Polynomial of R; :: thesis: for n being Nat holds p <> n
let u be Nat; :: thesis: p <> u
reconsider n = u as Element of NAT by ORDINAL1:def 12;

now :: thesis: not p = n

assume A1: p = n ; :: thesis: contradiction
dom p = NAT by FUNCT_2:def 1;
then consider i being Nat such that
A2: ( i = [n,(p . n)] & i < n ) by A1;
thus contradiction by A2; :: thesis: verum

end;

hence p <> u ; :: thesis: verum