let p be Polynomial of F_Real; :: thesis: ( p <> 0_. F_Real implies len p = (len (poly_diff p)) + 1 )
assume p <> 0_. F_Real ; :: thesis: len p = (len (poly_diff p)) + 1
then len (poly_diff p) = (len p) - 1 by Th44;
hence len p = (len (poly_diff p)) + 1 ; :: thesis: verum