let p be Polynomial of F_Real; :: thesis: ( p <> 0_. F_Real implies len (poly_diff p) = (len p) - 1 )
set x = (len p) - 1;
set d = poly_diff p;
assume p <> 0_. F_Real ; :: thesis: len (poly_diff p) = (len p) - 1
then A1: deg p <> - 1 by HURWITZ:20;
0 - 1 <= (len p) - 1 by XREAL_1:9;
then (- 1) + 1 < ((len p) - 1) + 1 by A1;
then (len p) - 1 >= 0 by INT_1:7;
then reconsider x = (len p) - 1 as Element of NAT by INT_1:3;
A2: x is_at_least_length_of poly_diff p

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not x <= i or (poly_diff p) . i = 0. F_Real )
assume i >= x ; :: thesis: (poly_diff p) . i = 0. F_Real
then i + 1 >= x + 1 by XREAL_1:6;
then p . (i + 1) = 0. F_Real by ALGSEQ_1:8;
hence 0. F_Real = (p . (i + 1)) * (i + 1)
.= (poly_diff p) . i by Def5 ;
:: thesis: verum

end;

for n being Nat st n is_at_least_length_of poly_diff p holds
x <= n

proof

let n be Nat; :: thesis: ( n is_at_least_length_of poly_diff p implies x <= n )
assume A3: n is_at_least_length_of poly_diff p ; :: thesis: x <= n

per cases ( x = 0 or x > 0 ) ;

suppose x = 0 ; :: thesis: x <= n

hence x <= n ; :: thesis: verum

end;

suppose x > 0 ; :: thesis: x <= n

then A4: x >= 0 + 1 by INT_1:7;
len p = x + 1 ;
then A5: p . x <> 0. F_Real by ALGSEQ_1:10;
reconsider x1 = x - 1 as Element of NAT by A4, NAT_1:21;
A6: (poly_diff p) . x1 = (p . (x1 + 1)) * (x1 + 1) by Def5;
assume x > n ; :: thesis: contradiction
then x >= n + 1 by INT_1:7;
then x1 >= (n + 1) - 1 by XREAL_1:9;
hence contradiction by A5, A3, A6; :: thesis: verum

end;

end;

end;

hence len (poly_diff p) = (len p) - 1 by A2, ALGSEQ_1:def 3; :: thesis: verum