let R be Ring; :: thesis: for p being Polynomial of R
for i being Integer holds p <> i
let p be Polynomial of R; :: thesis: for i being Integer holds p <> i
let i be Integer; :: thesis: p <> i
A1: i in INT by INT_1:def 2;

now :: thesis: not p = i

assume A2: p = i ; :: thesis: contradiction

per cases ( i in NAT or i in [:{0},NAT:] ) by A1, NUMBERS:def 4, XBOOLE_0:def 3;

suppose i in NAT ; :: thesis: contradiction

then reconsider n = i as Element of NAT ;
p = n by A2;
hence contradiction by Th18; :: thesis: verum

end;

suppose i in [:{0},NAT:] ; :: thesis: contradiction

then consider x, y being object such that
A3: ( x in {0} & y in NAT & i = [x,y] ) by ZFMISC_1:def 2;
reconsider n = y as Element of NAT by A3;
A4: p = [0,n] by A2, A3, TARSKI:def 1
.= {{0,n},{0}} by TARSKI:def 5 ;
A5: dom p = NAT by FUNCT_2:def 1;

per cases ( [0,(p . 0)] = {0,n} or [0,(p . 0)] = {0} ) by A4, A5;

suppose A6: [0,(p . 0)] = {0,n} ; :: thesis: contradiction

[0,(p . 0)] = {{0,(p . 0)},{0}} by TARSKI:def 5;
then A7: 0 in {{0,(p . 0)},{0}} by A6, TARSKI:def 2;

per cases ( 0 = {0} or 0 = {0,(p . 0)} ) by A7;

suppose 0 = {0} ; :: thesis: contradiction

hence contradiction by CARD_1:49; :: thesis: verum

end;

suppose 0 = {0,(p . 0)} ; :: thesis: contradiction

then {} = {0,(p . 0)} ;
hence contradiction ; :: thesis: verum

end;

end;

end;

suppose [0,(p . 0)] = {0} ; :: thesis: contradiction

hence contradiction by CARD_1:49; :: thesis: verum

end;

end;

end;

end;

end;

hence p <> i ; :: thesis: verum