theorem Th59: :: POLYDIFF:59

for p being Polynomial of F_Real holds Eval (Leading-Monomial p) = (p . ((len p) -' 1)) (#) (#Z ((len p) -' 1))