theorem Th1: :: WSIERP_1:1

for x being Complex holds
( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 )