:: deftheorem defines X^2+ FIELD_9:def 8 :
for R being Ring
for a being Element of R holds X^2+ a = <%a,(0. R),(1. R)%>;