theorem Th1: :: POLYEQ_5:1

for a being Complex holds a * a = a |^ 2