:: deftheorem defines eval RATFUNC1:def 19 :
for L being Field
for z being rational_function of L
for x being Element of L holds eval (z,x) = (eval ((z `1),x)) / (eval ((z `2),x));