let n1, n2 be Nat; :: thesis: ( n1 ^2 = n2 ^2 implies n1 = n2 )
assume n1 ^2 = n2 ^2 ; :: thesis: n1 = n2
then n1 = sqrt (n2 ^2) by SQUARE_1:22;
hence n1 = n2 by SQUARE_1:22; :: thesis: verum