:: deftheorem defines X^ FIELD_16:def 7 :
for R being non empty unital doubleLoopStr
for n being non trivial Nat holds X^ (n,R) = (0_. R) +* ((1,n) --> ((- (1. R)),(1. R)));