let x be Complex; :: thesis: ( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 )
A1: (- x) |^ 1 = - x ;
A2: x = x |^ 1 ;
then x |^ (1 + 1) = x * x by NEWTON:8;
then x |^ 2 = (- x) * (- x)
.= (- x) |^ (1 + 1) by A1, NEWTON:8 ;
hence ( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 ) by A2, NEWTON:8; :: thesis: verum