let L be algebraic-closed domRing; :: thesis: for p being non-zero Polynomial of L holds degree (BRoots p) = (len p) -' 1
let p be non-zero Polynomial of L; :: thesis: degree (BRoots p) = (len p) -' 1
defpred S₁[ Nat] means for p being non-zero Polynomial of L st len p = $1 & $1 > 0 holds
degree (BRoots p) = (len p) -' 1;
A1: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A2: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
let p be non-zero Polynomial of L; :: thesis: ( len p = k & k > 0 implies degree (BRoots p) = (len p) -' 1 )
assume that
A3: len p = k and
A4: k > 0 ; :: thesis: degree (BRoots p) = (len p) -' 1
A5: k >= 0 + 1 by A4, NAT_1:13;
thus degree (BRoots p) = (len p) -' 1 :: thesis: verum

proof

per cases ( k = 1 or k > 1 ) by A5, XXREAL_0:1;

suppose A6: k = 1 ; :: thesis: degree (BRoots p) = (len p) -' 1

hence degree (BRoots p) = 1 - 1 by A3, Th54
.= (len p) -' 1 by A3, A6, XREAL_1:233 ;
:: thesis: verum

end;

suppose A7: k > 1 ; :: thesis: degree (BRoots p) = (len p) -' 1

then p is with_roots by A3, POLYNOM5:def 9;
then consider x being Element of L such that
A8: x is_a_root_of p ;
A9: multiplicity (p,x) >= 1 by A8, Th49;
set r = <%(- x),(1. L)%>;
consider F being non empty finite Subset of NAT such that
A10: F = { l where l is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ l) *' q } and
A11: multiplicity (p,x) = max F by Def7;
max F in F by XXREAL_2:def 8;
then consider l being Element of NAT such that
A12: l = max F and
A13: ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ l) *' q by A10;
set rr = <%(- x),(1. L)%> `^ l;
consider q being Polynomial of L such that
A14: p = (<%(- x),(1. L)%> `^ l) *' q by A13;
reconsider q = q as non-zero Polynomial of L by A14, Th31;
len q > 0 by Th14;
then A15: len q >= 0 + 1 by NAT_1:13;
thus degree (BRoots p) = (len p) -' 1 :: thesis: verum

proof

len q > 0 by Th14;
then A16: q . ((len q) -' 1) <> 0. L by Th15;
len (<%(- x),(1. L)%> `^ l) > 0 by Th14;
then (<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1) <> 0. L by Th15;
then A17: ((<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1)) * (q . ((len q) -' 1)) <> 0. L by A16, VECTSP_2:def 1;
A18: ((l * 2) - l) + 1 = l + 1 ;
A19: len <%(- x),(1. L)%> = 2 by POLYNOM5:40;
then A20: len (<%(- x),(1. L)%> `^ l) = ((l * 2) - l) + 1 by POLYNOM5:23;
then A21: len (<%(- x),(1. L)%> `^ l) > 1 by A9, A11, A12, NAT_1:13;

per cases ( len q = 1 or len q > 1 ) by A15, XXREAL_0:1;

suppose A22: len q = 1 ; :: thesis: degree (BRoots p) = (len p) -' 1

A23: len p = ((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1 by A14, A17, POLYNOM4:10
.= len (<%(- x),(1. L)%> `^ l) by A22 ;
thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A14, Lm2
.= (degree (BRoots (<%(- x),(1. L)%> `^ l))) + 0 by A22, Th54
.= (((2 * l) - l) + 1) - 1 by Th55
.= (len p) -' 1 by A3, A5, A20, A23, XREAL_1:233 ; :: thesis: verum

end;

suppose A24: len q > 1 ; :: thesis: degree (BRoots p) = (len p) -' 1

then A25: ( degree (BRoots (<%(- x),(1. L)%> `^ l)) = (l + 1) -' 1 & degree (BRoots q) = (len q) -' 1 ) by A2, A3, A14, A20, A21, Th33;
thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A14, Lm2
.= ((len (<%(- x),(1. L)%> `^ l)) -' 1) + ((len q) -' 1) by A19, A18, A25, POLYNOM5:23
.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) -' 1) by A21, XREAL_1:233
.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) - 1) by A24, XREAL_1:233
.= (((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1) - 1
.= (len p) - 1 by A14, A17, POLYNOM4:10
.= (len p) -' 1 by A3, A7, XREAL_1:233 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

A26: for n being Nat holds S₁[n] from NAT_1:sch 4(A1);
len p > 0 by Th14;
hence degree (BRoots p) = (len p) -' 1 by A26; :: thesis: verum