let x be real number ; :: thesis: ( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 )
A1: (- x) |^ 1 = - x by NEWTON:5;
A2: x = x |^ 1 by NEWTON:5;
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