:: deftheorem defines X- FIELD_9:def 2 :
for R being Ring
for a being Element of R holds X- a = rpoly (1,a);