theorem :: RATFUNC1:32

for L being Field
for x being Element of L holds eval ((1._ L),x) = 1. L