let x be Real; :: thesis: x ^2 = x |^ 2
x ^2 = (x |^ 1) * x
.= x |^ (1 + 1) by NEWTON:6
.= x |^ 2 ;
hence x ^2 = x |^ 2 ; :: thesis: verum