:: deftheorem defines X^ FIELD_15:def 2 :
for R being non empty unital doubleLoopStr
for a being Element of R
for n being non zero Nat holds X^ (n,a) = (0_. R) +* ((0,n) --> ((- a),(1. R)));