theorem :: SQUARE_1:7

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