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;

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;

end;

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

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

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

end;

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

end;

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

end;

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