for i, n being Nat st ChangeVal_2 (i,n) = 1 holds
i = 1