for i, n being Nat st i is_expressible_by n holds
ChangeVal_2 (i,n) is_expressible_by n by Def8;