let n be Nat; :: thesis: n |^ 2 = n ^2
n |^ 2 = n |^ (1 + 1)
.= (n |^ 1) * (n |^ 1) by NEWTON:8
.= n ^2 ;
hence n |^ 2 = n ^2 ; :: thesis: verum