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;

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

hence
p <> r
; :: thesis: verumassume 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;

end;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;

end;

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;

end;x in {x,y} by TARSKI:def 2;