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

now :: thesis:

assume A2: p = r ; :: thesis:
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 = {x,y} or [1,(p . 1)] = {x} ) by A4, TARSKI:def 2;

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

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

per cases by A5, TARSKI:def 2;

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

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

end;

suppose x = {1} ; :: thesis:

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

end;

end;

end;

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

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

end;

end;

end;

hence p <> r ; :: thesis: