let R be Ring; for p being Polynomial of R
for r being Rational holds p <> r
let p be Polynomial of R; for r being Rational holds p <> r
let r be Rational; p <> r
A1:
r in (RAT+ \/ [:{0},RAT+:]) \ {[0,0]}
by NUMBERS:def 3, RAT_1:def 2;
now not p = rassume A2:
p = r
;
contradictionthen
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;
end;
hence
p <> r
; verum