:: deftheorem defines ^2 O_RING_1:def 1 :
for R being non empty doubleLoopStr
for x being Scalar of R holds x ^2 = x * x;