theorem tevale: :: FIELD_16:36

for R being non degenerated Ring
for S being RingExtension of R
for n being non trivial Nat
for a being Element of S holds Ext_eval ((X^ (n,R)),a) = (a |^ n) - a