let n be Element of NAT ; :: thesis: for a1, a2 being Element of NAT st a1 is_expressible_by n & a2 is_expressible_by n & ChangeVal_1 a1,n = ChangeVal_1 a2,n holds
a1 = a2
let a1, a2 be Element of NAT ; :: thesis: ( a1 is_expressible_by n & a2 is_expressible_by n & ChangeVal_1 a1,n = ChangeVal_1 a2,n implies a1 = a2 )
assume A1: ( a1 is_expressible_by n & a2 is_expressible_by n & ChangeVal_1 a1,n = ChangeVal_1 a2,n ) ; :: thesis: a1 = a2
then A2: a1 <> 2 to_power n by Def3;
A3: a2 <> 2 to_power n by A1, Def3;

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

suppose A4: ChangeVal_1 a1,n = 2 to_power n ; :: thesis: a1 = a2

hence a2 = 0 by A1, A3, Def7
.= a1 by A2, A4, Def7 ;
:: thesis: verum

end;

suppose A5: ChangeVal_1 a1,n <> 2 to_power n ; :: thesis: a1 = a2

hence a2 = ChangeVal_1 a1,n by A1, Def7
.= a1 by A5, Def7 ;
:: thesis: verum

end;

end;