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