theorem :: SQUARE_1:5

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