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