let R be Ring; :: thesis:
let p be Polynomial of R; :: thesis:
let r be Rational; :: thesis:
assume A1: ( r in RAT+ & p = r ) ; :: thesis:
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,j} or {{i,(p . i)},{i}} = {i} ) by A5, TARSKI:def 2;

suppose A6: {{i,(p . i)},{i}} = {i,j} ; :: thesis:

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

per cases by A6, A7, TARSKI:def 2;

suppose j = {i} ; :: thesis:

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

end;

suppose A8: j = {i,(p . i)} ; :: thesis:

per cases ;

suppose i = p . i ; :: thesis:

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:

end;

suppose i <> p . i ; :: thesis:

per cases by A8, Th3;

suppose ( i = 1 & p . i = 0 ) ; :: thesis:

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

end;

suppose ( i = 0 & p . i = 1 ) ; :: thesis:

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

end;

end;

end;

end;

end;

end;

end;

suppose A11: {{i,(p . i)},{i}} = {i} ; :: thesis:

{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:

end;

end;