let R be Ring; :: thesis: for p being Polynomial of R
for r being Real holds p <> r
let p be Polynomial of R; :: thesis: for r being Real holds p <> r
let r be Real; :: thesis: p <> r
A1: r in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} by XREAL_0:def 1, NUMBERS:def 1;

now :: thesis: not p = r

assume A2: p = r ; :: thesis: contradiction
then not r in REAL+ by Lem4;
then r in [:{0},REAL+:] by A1, XBOOLE_0:def 3;
then consider x, y being object such that
A3: ( x in {0} & y in REAL+ & 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;
x in {x,y} by TARSKI:def 2;

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

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

then x <> {} ;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;

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

then x <> {} ;
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