theorem :: POLYDIFF:58

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