for n1, n2 being Nat st n1 ^2 = n2 ^2 holds
n1 = n2