for i, n being Nat st i is_expressible_by n holds
( ChangeVal_1 (i,n) <= 2 to_power n & ChangeVal_1 (i,n) > 0 )