:: deftheorem defines ^2 POLYEQ_3:def 1 :
for z being Element of COMPLEX holds z ^2 = (((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>);