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

assume A2: for n being Nat st n < k holds
S1[n] ; :: thesis: S1[k]
let p be non-zero Polynomial of L; :: thesis: ( len p = k & k > 0 implies degree () = (len p) -' 1 )
assume that
A3: len p = k and
A4: k > 0 ; :: thesis: degree () = (len p) -' 1
A5: k >= 0 + 1 by ;
thus degree () = (len p) -' 1 :: thesis: verum
proof
per cases ( k = 1 or k > 1 ) by ;
suppose A6: k = 1 ; :: thesis: degree () = (len p) -' 1
hence degree () = 1 - 1 by
.= (len p) -' 1 by ;
:: thesis: verum
end;
suppose A7: k > 1 ; :: thesis: degree () = (len p) -' 1
then p is with_roots by ;
then consider x being Element of L such that
A8: x is_a_root_of p ;
A9: multiplicity (p,x) >= 1 by ;
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 ;
len q > 0 by Th14;
then A15: len q >= 0 + 1 by NAT_1:13;
thus degree () = (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 ;
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 ;
per cases ( len q = 1 or len q > 1 ) by ;
suppose A22: len q = 1 ; :: thesis: degree () = (len p) -' 1
A23: len p = ((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1 by
.= len (<%(- x),(1. L)%> `^ l) by A22 ;
thus degree () = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree ()) by
.= (degree (BRoots (<%(- x),(1. L)%> `^ l))) + 0 by
.= (((2 * l) - l) + 1) - 1 by Th55
.= (len p) -' 1 by ; :: thesis: verum
end;
suppose A24: len q > 1 ; :: thesis: degree () = (len p) -' 1
then A25: ( degree (BRoots (<%(- x),(1. L)%> `^ l)) = (l + 1) -' 1 & degree () = (len q) -' 1 ) by A2, A3, A14, A20, A21, Th33;
thus degree () = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree ()) by
.= ((len (<%(- x),(1. L)%> `^ l)) -' 1) + ((len q) -' 1) by
.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) -' 1) by
.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) - 1) by
.= (((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1) - 1
.= (len p) - 1 by
.= (len p) -' 1 by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A26: for n being Nat holds S1[n] from len p > 0 by Th14;
hence degree () = (len p) -' 1 by A26; :: thesis: verum