for R being domRing
for S being domRingExtension of R
for n being non zero Element of NAT
for a being Element of S holds Ext_eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n