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