let R be domRing; :: thesis: for p, q being Polynomial of R st ex S being Subset of R st
( card S = (max ((deg p),(deg q))) + 1 & ( for a being Element of R st a in S holds
eval (p,a) = eval (q,a) ) ) holds
p = q
let p, q be Polynomial of R; :: thesis: ( ex S being Subset of R st
( card S = (max ((deg p),(deg q))) + 1 & ( for a being Element of R st a in S holds
eval (p,a) = eval (q,a) ) ) implies p = q )
assume ex S being Subset of R st
( card S = (max ((deg p),(deg q))) + 1 & ( for a being Element of R st a in S holds
eval (p,a) = eval (q,a) ) ) ; :: thesis: p = q
then consider S being Subset of R such that
A0: ( card S = (max ((deg p),(deg q))) + 1 & ( for a being Element of R st a in S holds
eval (p,a) = eval (q,a) ) ) ;

now :: thesis: not p <> q

assume HH: p <> q ; :: thesis: contradiction
(max ((deg p),(deg q))) + 1 is Element of NAT

proof

D: max ((deg p),(deg q)) >= deg p by XXREAL_0:25;
deg p >= - 1

proof

per cases ( p = 0_. R or p <> 0_. R ) ;

suppose p = 0_. R ; :: thesis: deg p >= - 1

hence deg p >= - 1 by HURWITZ:20; :: thesis: verum

end;

suppose p <> 0_. R ; :: thesis: deg p >= - 1

hence deg p >= - 1 by T8; :: thesis: verum

end;

end;

end;

then max ((deg p),(deg q)) >= - 1 by D, XXREAL_0:2;
then (max ((deg p),(deg q))) + 1 >= (- 1) + 1 by XREAL_1:6;
hence (max ((deg p),(deg q))) + 1 is Element of NAT by INT_1:3; :: thesis: verum

end;

then reconsider S = S as finite Subset of the carrier of R by A0;

per cases ( p is zero or not p is zero ) ;

suppose AS: p is zero ; :: thesis: contradiction

then not q is zero by HH;
then reconsider q = q as non zero Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
reconsider n = deg q as Element of NAT by AS, T8;
deg p = - 1 by AS, HURWITZ:20;
then C0: (max ((deg p),(deg q))) + 1 = n + 1 by XXREAL_0:def 10;

now :: thesis: for x being object st x in S holds
x in Roots q

let x be object ; :: thesis: ( x in S implies x in Roots q )
assume C: x in S ; :: thesis: x in Roots q
then reconsider a = x as Element of R ;
eval (q,a) = eval (p,a) by A0, C
.= 0. R by AS, POLYNOM4:17 ;
then a is_a_root_of q by POLYNOM5:def 7;
hence x in Roots q by POLYNOM5:def 10; :: thesis: verum

end;

then C2: n + 1 <= card (Roots q) by A0, C0, NAT_1:43, TARSKI:def 3;
card (Roots q) <= deg q by degpoly;
then C4: n + 1 <= n by C2, XXREAL_0:2;
n <= n + 1 by NAT_1:11;
then n + 1 = n by C4, XXREAL_0:1;
hence contradiction ; :: thesis: verum

end;

suppose not p is zero ; :: thesis: contradiction

then reconsider n = deg p as Element of NAT by T8;
H2: n = (len p) - 1 by HURWITZ:def 2;
then H2a: len p = n + 1 ;

per cases ( len q < len p or len p < len q or len p = len q ) by XXREAL_0:1;

suppose D: len q < len p ; :: thesis: contradiction

then (len q) + 1 <= len p by INT_1:7;
then ((len q) + 1) - 1 <= (len p) - 1 by XREAL_1:9;
then q . n = 0. R by H2, ALGSEQ_1:8;
then H3: q . n <> p . n by H2a, ALGSEQ_1:10;
( deg q = (len q) - 1 & deg p = (len p) - 1 ) by HURWITZ:def 2;
then H4: max ((deg p),(deg q)) = n by D, XREAL_1:9, XXREAL_0:def 10;
defpred S₁[ Nat] means p . $1 <> q . $1;
A2: for k being Nat st S₁[k] holds
k <= n

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= n )
assume B0: S₁[k] ; :: thesis: k <= n

now :: thesis: for i being Nat st i > n holds
p . i = q . i

let i be Nat; :: thesis: ( i > n implies p . i = q . i )
assume i > n ; :: thesis: p . i = q . i
then B1: i >= len p by H2a, NAT_1:13;
hence p . i = 0. R by ALGSEQ_1:8
.= q . i by B1, D, XXREAL_0:2, ALGSEQ_1:8 ;
:: thesis: verum

end;

hence k <= n by B0; :: thesis: verum

end;

A3: ex k being Nat st S₁[k] by H3;
consider m being Nat such that
A4: ( S₁[m] & ( for i being Nat st S₁[i] holds
i <= m ) ) from NAT_1:sch 6(A2, A3);
A5: ( p . m <> q . m & m <= n ) by A2, A4;

A6: now :: thesis: not (p - q) . m = 0. R

assume A7: (p - q) . m = 0. R ; :: thesis: contradiction
(p . m) + (0. R) = (p . m) + ((- (q . m)) + (q . m)) by RLVECT_1:5
.= ((p . m) + (- (q . m))) + (q . m) by RLVECT_1:def 3
.= ((p . m) - (q . m)) + (q . m) by RLVECT_1:def 11
.= (0. R) + (q . m) by A7, NORMSP_1:def 3 ;
hence contradiction by A4; :: thesis: verum

end;

then p - q <> 0_. R by FUNCOP_1:7, ORDINAL1:def 12;
then reconsider r = p - q as non zero Polynomial of R by UPROOTS:def 5;

now :: thesis: for x being object st x in S holds
x in Roots r

let x be object ; :: thesis: ( x in S implies x in Roots r )
assume C2: x in S ; :: thesis: x in Roots r
then reconsider a = x as Element of R ;
eval (r,a) = (eval (p,a)) - (eval (q,a)) by POLYNOM4:21
.= (eval (p,a)) - (eval (p,a)) by C2, A0
.= 0. R by RLVECT_1:15 ;
then a is_a_root_of r by POLYNOM5:def 7;
hence x in Roots r by POLYNOM5:def 10; :: thesis: verum

end;

then C2: n + 1 <= card (Roots r) by A0, H4, NAT_1:43, TARSKI:def 3;
len r = m + 1

proof

E1: now :: thesis: for i being Nat st i >= m + 1 holds
r . i = 0. R

let i be Nat; :: thesis: ( i >= m + 1 implies r . i = 0. R )
assume i >= m + 1 ; :: thesis: r . i = 0. R
then not i <= m by NAT_1:13;
then X: p . i = q . i by A4;
thus r . i = (p . i) - (q . i) by NORMSP_1:def 3
.= 0. R by X, RLVECT_1:15 ; :: thesis: verum

end;

for k being Nat st k is_at_least_length_of r holds
m + 1 <= k by A6, NAT_1:13;
hence len r = m + 1 by E1, ALGSEQ_1:def 2, ALGSEQ_1:def 3; :: thesis: verum

end;

then (len r) - 1 = m ;
then C3: deg r = m by HURWITZ:def 2;
card (Roots r) <= deg r by degpoly;
then n + 1 <= m by C2, C3, XXREAL_0:2;
then C4: n + 1 <= n by A5, XXREAL_0:2;
n <= n + 1 by NAT_1:11;
then n + 1 = n by C4, XXREAL_0:1;
hence contradiction ; :: thesis: verum

end;

suppose D: len p < len q ; :: thesis: contradiction

then (len p) + 1 <= len q by INT_1:7;
then D1: ((len p) + 1) - 1 <= (len q) - 1 by XREAL_1:9;
(len p) - 1 < (len q) - 1 by D, XREAL_1:9;
then deg p < (len q) - 1 by HURWITZ:def 2;
then ( deg p < deg q & 0 <= n ) by HURWITZ:def 2;
then reconsider l = deg q as Element of NAT by INT_1:3;
H2b: l = (len q) - 1 by HURWITZ:def 2;
then H2c: len q = l + 1 ;
p . l = 0. R by D1, H2b, ALGSEQ_1:8;
then H3: q . l <> p . l by H2c, ALGSEQ_1:10;
( deg q = (len q) - 1 & deg p = (len p) - 1 ) by HURWITZ:def 2;
then H4: max ((deg p),(deg q)) = l by D, XREAL_1:9, XXREAL_0:def 10;
defpred S₁[ Nat] means p . $1 <> q . $1;
A2: for k being Nat st S₁[k] holds
k <= l

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= l )
assume B0: S₁[k] ; :: thesis: k <= l

now :: thesis: for i being Nat st i > l holds
q . i = p . i

let i be Nat; :: thesis: ( i > l implies q . i = p . i )
assume i > l ; :: thesis: q . i = p . i
then B1: i >= len q by H2c, NAT_1:13;
hence q . i = 0. R by ALGSEQ_1:8
.= p . i by B1, D, XXREAL_0:2, ALGSEQ_1:8 ;
:: thesis: verum

end;

hence k <= l by B0; :: thesis: verum

end;

A3: ex k being Nat st S₁[k] by H3;
consider m being Nat such that
A4: ( S₁[m] & ( for i being Nat st S₁[i] holds
i <= m ) ) from NAT_1:sch 6(A2, A3);
A5: ( p . m <> q . m & m <= l ) by A2, A4;

A6: now :: thesis: not (p - q) . m = 0. R

assume A7: (p - q) . m = 0. R ; :: thesis: contradiction
(p . m) + (0. R) = (p . m) + ((- (q . m)) + (q . m)) by RLVECT_1:5
.= ((p . m) + (- (q . m))) + (q . m) by RLVECT_1:def 3
.= ((p . m) - (q . m)) + (q . m) by RLVECT_1:def 11
.= (0. R) + (q . m) by A7, NORMSP_1:def 3 ;
hence contradiction by A4; :: thesis: verum

end;

then p - q <> 0_. R by FUNCOP_1:7, ORDINAL1:def 12;
then reconsider r = p - q as non zero Polynomial of R by UPROOTS:def 5;

now :: thesis: for x being object st x in S holds
x in Roots r

let x be object ; :: thesis: ( x in S implies x in Roots r )
assume C2: x in S ; :: thesis: x in Roots r
then reconsider a = x as Element of R ;
eval (r,a) = (eval (p,a)) - (eval (q,a)) by POLYNOM4:21
.= (eval (p,a)) - (eval (p,a)) by C2, A0
.= 0. R by RLVECT_1:15 ;
then a is_a_root_of r by POLYNOM5:def 7;
hence x in Roots r by POLYNOM5:def 10; :: thesis: verum

end;

then C2: l + 1 <= card (Roots r) by A0, H4, NAT_1:43, TARSKI:def 3;
len r = m + 1

proof

E1: now :: thesis: for i being Nat st i >= m + 1 holds
r . i = 0. R

let i be Nat; :: thesis: ( i >= m + 1 implies r . i = 0. R )
assume i >= m + 1 ; :: thesis: r . i = 0. R
then not i <= m by NAT_1:13;
then X: p . i = q . i by A4;
thus r . i = (p . i) - (q . i) by NORMSP_1:def 3
.= 0. R by X, RLVECT_1:15 ; :: thesis: verum

end;

for k being Nat st k is_at_least_length_of r holds
m + 1 <= k by A6, NAT_1:13;
hence len r = m + 1 by E1, ALGSEQ_1:def 2, ALGSEQ_1:def 3; :: thesis: verum

end;

then (len r) - 1 = m ;
then C3: deg r = m by HURWITZ:def 2;
card (Roots r) <= deg r by degpoly;
then l + 1 <= m by C2, C3, XXREAL_0:2;
then C4: l + 1 <= l by A5, XXREAL_0:2;
l <= l + 1 by NAT_1:11;
then l + 1 = l by C4, XXREAL_0:1;
hence contradiction ; :: thesis: verum

end;

suppose D: len p = len q ; :: thesis: contradiction

n = (len p) - 1 by HURWITZ:def 2;
then H2: len p = n + 1 ;
H4: ( deg q = (len q) - 1 & deg p = (len p) - 1 ) by HURWITZ:def 2;
consider k being Nat such that
A1: ( k < len p & p . k <> q . k ) by HH, D, ALGSEQ_1:12;
defpred S₁[ Nat] means p . $1 <> q . $1;
A2: for k being Nat st S₁[k] holds
k <= n

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= n )
assume B0: S₁[k] ; :: thesis: k <= n

now :: thesis: for i being Nat st i > n holds
p . i = q . i

let i be Nat; :: thesis: ( i > n implies p . i = q . i )
assume i > n ; :: thesis: p . i = q . i
then B1: i >= len p by H2, NAT_1:13;
hence p . i = 0. R by ALGSEQ_1:8
.= q . i by D, B1, ALGSEQ_1:8 ;
:: thesis: verum

end;

hence k <= n by B0; :: thesis: verum

end;

A3: ex k being Nat st S₁[k] by A1;
consider m being Nat such that
A4: ( S₁[m] & ( for i being Nat st S₁[i] holds
i <= m ) ) from NAT_1:sch 6(A2, A3);
A5: ( p . m <> q . m & m <= n ) by A2, A4;

A6: now :: thesis: not (p - q) . m = 0. R

assume A7: (p - q) . m = 0. R ; :: thesis: contradiction
(p . m) + (0. R) = (p . m) + ((- (q . m)) + (q . m)) by RLVECT_1:5
.= ((p . m) + (- (q . m))) + (q . m) by RLVECT_1:def 3
.= ((p . m) - (q . m)) + (q . m) by RLVECT_1:def 11
.= (0. R) + (q . m) by A7, NORMSP_1:def 3 ;
hence contradiction by A4; :: thesis: verum

end;

then p - q <> 0_. R by FUNCOP_1:7, ORDINAL1:def 12;
then reconsider r = p - q as non zero Polynomial of R by UPROOTS:def 5;

now :: thesis: for x being object st x in S holds
x in Roots r

let x be object ; :: thesis: ( x in S implies x in Roots r )
assume C2: x in S ; :: thesis: x in Roots r
then reconsider a = x as Element of R ;
eval (r,a) = (eval (p,a)) - (eval (q,a)) by POLYNOM4:21
.= (eval (p,a)) - (eval (p,a)) by C2, A0
.= 0. R by RLVECT_1:15 ;
then a is_a_root_of r by POLYNOM5:def 7;
hence x in Roots r by POLYNOM5:def 10; :: thesis: verum

end;

then C2: n + 1 <= card (Roots r) by H4, A0, D, NAT_1:43, TARSKI:def 3;
len r = m + 1

proof

E1: now :: thesis: for i being Nat st i >= m + 1 holds
r . i = 0. R

let i be Nat; :: thesis: ( i >= m + 1 implies r . i = 0. R )
assume i >= m + 1 ; :: thesis: r . i = 0. R
then not i <= m by NAT_1:13;
then X: p . i = q . i by A4;
thus r . i = (p . i) - (q . i) by NORMSP_1:def 3
.= 0. R by X, RLVECT_1:15 ; :: thesis: verum

end;

for k being Nat st k is_at_least_length_of r holds
m + 1 <= k by A6, NAT_1:13;
hence len r = m + 1 by E1, ALGSEQ_1:def 2, ALGSEQ_1:def 3; :: thesis: verum

end;

then (len r) - 1 = m ;
then C3: deg r = m by HURWITZ:def 2;
card (Roots r) <= deg r by degpoly;
then n + 1 <= m by C2, C3, XXREAL_0:2;
then C4: n + 1 <= n by A5, XXREAL_0:2;
n <= n + 1 by NAT_1:11;
then n + 1 = n by C4, XXREAL_0:1;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

end;

hence p = q ; :: thesis: verum