theorem Th4: :: POLYEQ_5:4

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