theorem :: SQUARE_1:3

for a being Complex holds a ^2 = (- a) ^2 ;