let p be constant Polynomial of F_Real; :: thesis: poly_diff p = 0_. F_Real

per cases ( p <> 0_. F_Real or p = 0_. F_Real ) ;

suppose p <> 0_. F_Real ; :: thesis: poly_diff p = 0_. F_Real

then A1: len p = (len (poly_diff p)) + 1 by Th45;
deg p <= 0 by RATFUNC1:def 2;
then len (poly_diff p) = 0 by A1;
then deg (poly_diff p) = - 1 ;
hence poly_diff p = 0_. F_Real by HURWITZ:20; :: thesis: verum

end;

suppose A2: p = 0_. F_Real ; :: thesis: poly_diff p = 0_. F_Real

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (poly_diff p) . n = (0_. F_Real) . n
thus (0_. F_Real) . n = ((0_. F_Real) . (n + 1)) * (n + 1)
.= (poly_diff p) . n by A2, Def5 ; :: thesis: verum

end;

end;