theorem :: SQUARE_1:8

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