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
A1: len p > 0 by Th19;
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;
A2: 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 A3: 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
A4: len p = k and
A5: k > 0 ; :: thesis: degree (BRoots p) = (len p) -' 1
A6: k >= 0 + 1 by A5, NAT_1:13;
thus degree (BRoots p) = (len p) -' 1 :: thesis: verum

proof

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

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

hence degree (BRoots p) = 1 - 1 by A4, Th59
.= (len p) -' 1 by A4, A7, XREAL_1:235 ;
:: thesis: verum

end;

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

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

proof

A17: len <%(- x),(1. L)%> = 2 by POLYNOM5:41;
then A18: len (<%(- x),(1. L)%> `^ l) = ((l * 2) - l) + 1 by POLYNOM5:24;
A19: ((l * 2) - l) + 1 = l + 1 ;
A20: len (<%(- x),(1. L)%> `^ l) > 1 by A10, A12, A13, A18, NAT_1:13;
( len (<%(- x),(1. L)%> `^ l) > 0 & len q > 0 ) by Th19;
then ( (<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1) <> 0. L & q . ((len q) -' 1) <> 0. L ) by Th20;
then A21: ((<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1)) * (q . ((len q) -' 1)) <> 0. L by VECTSP_2:def 5;

per cases ( len q = 1 or len q > 1 ) by A16, 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 A15, A21, POLYNOM4:13
.= len (<%(- x),(1. L)%> `^ l) by A22 ;
thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A15, Lm2
.= (degree (BRoots (<%(- x),(1. L)%> `^ l))) + 0 by A22, Th59
.= (((2 * l) - l) + 1) - 1 by Th60
.= (len p) -' 1 by A4, A6, A18, A23, XREAL_1:235 ; :: 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 A3, A4, A15, A18, A20, Th38;
thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A15, Lm2
.= ((len (<%(- x),(1. L)%> `^ l)) -' 1) + ((len q) -' 1) by A17, A19, A25, POLYNOM5:24
.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) -' 1) by A20, XREAL_1:235
.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) - 1) by A24, XREAL_1:235
.= (((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1) - 1
.= (len p) - 1 by A15, A21, POLYNOM4:13
.= (len p) -' 1 by A4, A8, XREAL_1:235 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

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