theorem evconst: :: RING_5:8

for R being Ring
for a, b being Element of R holds eval ((a | R),b) = a