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

( 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

hence
p = q
; :: thesis: verumassume HH:
p <> q
; :: thesis: contradiction

(max ((deg p),(deg q))) + 1 is Element of NAT

end;(max ((deg p),(deg q))) + 1 is Element of NAT

proof

then reconsider S = S as finite Subset of the carrier of R by A0;
D:
max ((deg p),(deg q)) >= deg p
by XXREAL_0:25;

deg p >= - 1 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;deg p >= - 1 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

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

end;

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;

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

then C2:
n + 1 <= card (Roots q)
by A0, C0, NAT_1:43, TARSKI:def 3;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;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

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

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 ;

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

end;

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_{1}[ Nat] means p . $1 <> q . $1;

A2: for k being Nat st S_{1}[k] holds

k <= n_{1}[k]
by H3;

consider m being Nat such that

A4: ( S_{1}[m] & ( for i being Nat st S_{1}[i] holds

i <= m ) ) from NAT_1:sch 6(A2, A3);

A5: ( p . m <> q . m & m <= n ) by A2, A4;

then reconsider r = p - q as non zero Polynomial of R by UPROOTS:def 5;

len r = m + 1

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

A2: for k being Nat st S

k <= n

proof

A3:
ex k being Nat st S
let k be Nat; :: thesis: ( S_{1}[k] implies k <= n )

assume B0: S_{1}[k]
; :: thesis: k <= n

end;assume B0: S

now :: thesis: for i being Nat st i > n holds

p . i = q . i

hence
k <= n
by B0; :: thesis: verump . 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;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

consider m being Nat such that

A4: ( S

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

then
p - q <> 0_. R
by FUNCOP_1:7, ORDINAL1:def 12;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;(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

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

then C2:
n + 1 <= card (Roots r)
by A0, H4, NAT_1:43, TARSKI:def 3;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;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

len r = m + 1

proof

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
;E1: now :: thesis: for i being Nat st i >= m + 1 holds

r . i = 0. R

for k being Nat st k is_at_least_length_of r 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;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

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

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

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_{1}[ Nat] means p . $1 <> q . $1;

A2: for k being Nat st S_{1}[k] holds

k <= l_{1}[k]
by H3;

consider m being Nat such that

A4: ( S_{1}[m] & ( for i being Nat st S_{1}[i] holds

i <= m ) ) from NAT_1:sch 6(A2, A3);

A5: ( p . m <> q . m & m <= l ) by A2, A4;

then reconsider r = p - q as non zero Polynomial of R by UPROOTS:def 5;

len r = m + 1

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

A2: for k being Nat st S

k <= l

proof

A3:
ex k being Nat st S
let k be Nat; :: thesis: ( S_{1}[k] implies k <= l )

assume B0: S_{1}[k]
; :: thesis: k <= l

end;assume B0: S

now :: thesis: for i being Nat st i > l holds

q . i = p . i

hence
k <= l
by B0; :: thesis: verumq . 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;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

consider m being Nat such that

A4: ( S

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

then
p - q <> 0_. R
by FUNCOP_1:7, ORDINAL1:def 12;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;(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

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

then C2:
l + 1 <= card (Roots r)
by A0, H4, NAT_1:43, TARSKI:def 3;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;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

len r = m + 1

proof

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
;E1: now :: thesis: for i being Nat st i >= m + 1 holds

r . i = 0. R

for k being Nat st k is_at_least_length_of r 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;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

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

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

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_{1}[ Nat] means p . $1 <> q . $1;

A2: for k being Nat st S_{1}[k] holds

k <= n_{1}[k]
by A1;

consider m being Nat such that

A4: ( S_{1}[m] & ( for i being Nat st S_{1}[i] holds

i <= m ) ) from NAT_1:sch 6(A2, A3);

A5: ( p . m <> q . m & m <= n ) by A2, A4;

then reconsider r = p - q as non zero Polynomial of R by UPROOTS:def 5;

len r = m + 1

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

A2: for k being Nat st S

k <= n

proof

A3:
ex k being Nat st S
let k be Nat; :: thesis: ( S_{1}[k] implies k <= n )

assume B0: S_{1}[k]
; :: thesis: k <= n

end;assume B0: S

now :: thesis: for i being Nat st i > n holds

p . i = q . i

hence
k <= n
by B0; :: thesis: verump . 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;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

consider m being Nat such that

A4: ( S

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

then
p - q <> 0_. R
by FUNCOP_1:7, ORDINAL1:def 12;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;(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

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

then C2:
n + 1 <= card (Roots r)
by H4, A0, D, NAT_1:43, TARSKI:def 3;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;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

len r = m + 1

proof

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
;E1: now :: thesis: for i being Nat st i >= m + 1 holds

r . i = 0. R

for k being Nat st k is_at_least_length_of r 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;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

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

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