theorem :: IDEA_1:25

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