theorem Th1: :: NEWTON01:1

for a1, b1 being Complex holds (a1 |^ 2) - (b1 |^ 2) = (a1 - b1) * (a1 + b1)