let n, a1, a2 be Nat; :: thesis: ( a1 is_expressible_by n & a2 is_expressible_by n & ChangeVal_1 (a1,n) = ChangeVal_1 (a2,n) implies a1 = a2 )
assume that
A1: a1 is_expressible_by n and
A2: a2 is_expressible_by n and
A3: ChangeVal_1 (a1,n) = ChangeVal_1 (a2,n) ; :: thesis: a1 = a2
A4: a1 <> 2 to_power n by A1;
A5: a2 <> 2 to_power n by A2;

per cases ( ChangeVal_1 (a1,n) = 2 to_power n or ChangeVal_1 (a1,n) <> 2 to_power n ) ;

suppose A6: ChangeVal_1 (a1,n) = 2 to_power n ; :: thesis: a1 = a2

hence a2 = 0 by A3, A5, Def7
.= a1 by A4, A6, Def7 ;
:: thesis: verum

end;

suppose A7: ChangeVal_1 (a1,n) <> 2 to_power n ; :: thesis: a1 = a2

hence a2 = ChangeVal_1 (a1,n) by A3, Def7
.= a1 by A7, Def7 ;
:: thesis: verum

end;

end;