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