for n, a1, a2 being Nat st a1 is_expressible_by n & a2 is_expressible_by n & ChangeVal_1 (a1,n) = ChangeVal_1 (a2,n) holds
a1 = a2