for n being Nat st n >= 1 holds
n -root 0 = 0