:: deftheorem Def7 defines ChangeVal_1 IDEA_1:def 7 :
for n, i being Nat holds
( ( i = 0 implies ChangeVal_1 (i,n) = 2 to_power n ) & ( not i = 0 implies ChangeVal_1 (i,n) = i ) );