let m, n be Element of NAT ; :: thesis: ( m ^2 = n ^2 implies m = n )
assume A1: m ^2 = n ^2 ; :: thesis: m = n
per cases ( m = n or m = - n ) by A1, SQUARE_1:40;
suppose m = n ; :: thesis: m = n
hence m = n ; :: thesis: verum
end;
suppose A2: m = - n ; :: thesis: m = n
then m = - 0 ;
hence m = n by A2; :: thesis: verum
end;
end;