let R be Ring; :: thesis: for p being Polynomial of R
for r being Rational st r in RAT+ & p = r holds
r = [1,2]
let p be Polynomial of R; :: thesis: for r being Rational st r in RAT+ & p = r holds
r = [1,2]
let r be Rational; :: thesis: ( r in RAT+ & p = r implies r = [1,2] )
assume A1: ( r in RAT+ & p = r ) ; :: thesis: r = [1,2]
A2: dom p = NAT by FUNCT_2:def 1;
not r in omega by A1, Th19;
then r in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } by A1, XBOOLE_0:def 3;
then A3: ( r in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } & not r in { [k,1] where k is Element of omega : verum } ) by XBOOLE_0:def 5;
then consider i, j being Element of omega such that
A4: ( r = [i,j] & i,j are_coprime & j <> {} ) ;
[i,(p . i)] in p by A2, FUNCT_1:def 2;
then {{i,(p . i)},{i}} in p by TARSKI:def 5;
then A5: {{i,(p . i)},{i}} in {{i,j},{i}} by A1, A4, TARSKI:def 5;

per cases ( {{i,(p . i)},{i}} = {i,j} or {{i,(p . i)},{i}} = {i} ) by A5, TARSKI:def 2;

suppose A6: {{i,(p . i)},{i}} = {i,j} ; :: thesis: r = [1,2]

A7: j in {i,j} by TARSKI:def 2;

per cases ( j = {i} or j = {i,(p . i)} ) by A6, A7, TARSKI:def 2;

suppose j = {i} ; :: thesis: r = [1,2]

then i = 0 by Th2;
then j = 1 by A4, ARYTM_3:3;
hence r = [1,2] by A3, A4; :: thesis: verum

end;

suppose A8: j = {i,(p . i)} ; :: thesis: r = [1,2]

per cases ( i = p . i or i <> p . i ) ;

suppose i = p . i ; :: thesis: r = [1,2]

then for o being object holds
( o in j iff o = i ) by A8, TARSKI:def 2;
then j = {i} by TARSKI:def 1;
then i = {} by Th2;
then j = 1 by A4, ARYTM_3:3;
hence r = [1,2] by A3, A4; :: thesis: verum

end;

suppose i <> p . i ; :: thesis: r = [1,2]

per cases then ( ( i = 1 & p . i = 0 ) or ( i = 0 & p . i = 1 ) ) by A8, Th3;

suppose ( i = 1 & p . i = 0 ) ; :: thesis: r = [1,2]

hence r = [1,2] by A8, A4, CARD_1:50; :: thesis: verum

end;

suppose ( i = 0 & p . i = 1 ) ; :: thesis: r = [1,2]

then j = 1 by A4, ARYTM_3:3;
hence r = [1,2] by A3, A4; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose A11: {{i,(p . i)},{i}} = {i} ; :: thesis: r = [1,2]

{i,(p . i)} in {{i,(p . i)},{i}} by TARSKI:def 2;
then {i,(p . i)} = i by A11, TARSKI:def 1;
then i in i by TARSKI:def 2;
hence r = [1,2] ; :: thesis: verum

end;

end;