:: deftheorem defines ^2 SQUARE_1:def 1 :
for x being Complex holds x ^2 = x * x;