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 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, Def3;
A5: a2 <> 2 to_power n by A2, Def3;

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;