theorem :: SQUARE_1:9

for a, b being Complex holds (a * b) ^2 = (a ^2) * (b ^2) ;