let R be Ring; :: thesis: for p being Polynomial of R
for r being Rational holds p <> r
let p be Polynomial of R; :: thesis: for r being Rational holds p <> r
let r be Rational; :: thesis: p <> r
A1: r in (RAT+ \/ [:{0},RAT+:]) \ {[0,0]} by NUMBERS:def 3, RAT_1:def 2;

now :: thesis: not p = r

assume A2: p = r ; :: thesis: contradiction
then not r in RAT+ by Lem2, Lem3;
then r in [:{0},RAT+:] by A1, XBOOLE_0:def 3;
then consider x, y being object such that
A3: ( x in {0} & y in RAT+ & r = [x,y] ) by ZFMISC_1:def 2;
dom p = NAT by FUNCT_2:def 1;
then [1,(p . 1)] in p by FUNCT_1:def 2;
then A4: [1,(p . 1)] in {{x,y},{x}} by A3, A2, TARSKI:def 5;

per cases ( [1,(p . 1)] = {x,y} or [1,(p . 1)] = {x} ) by A4, TARSKI:def 2;

suppose [1,(p . 1)] = {x,y} ; :: thesis: contradiction

then A5: {{1,(p . 1)},{1}} = {x,y} by TARSKI:def 5;
A6: x in {x,y} by TARSKI:def 2;

per cases ( x = {1,(p . 1)} or x = {1} ) by A5, A6, TARSKI:def 2;

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

hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;

suppose x = {1} ; :: thesis: contradiction

hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

hence contradiction by A3, TARSKI:def 1, CARD_1:49; :: thesis: verum

end;

end;

end;

hence p <> r ; :: thesis: verum