:: deftheorem defines Eval POLYDIFF:def 6 :
for p being Polynomial of F_Real holds Eval p = Polynomial-Function (F_Real,p);