let n be Element of NAT ; :: thesis: for a1, a2 being Element of NAT st a1 <> 0 & a2 <> 0 & ChangeVal_2 a1,n = ChangeVal_2 a2,n holds
a1 = a2
let a1, a2 be Element of NAT ; :: thesis: ( a1 <> 0 & a2 <> 0 & ChangeVal_2 a1,n = ChangeVal_2 a2,n implies a1 = a2 )
assume A1: ( a1 <> 0 & a2 <> 0 & ChangeVal_2 a1,n = ChangeVal_2 a2,n ) ; :: thesis: a1 = a2

per cases ( ChangeVal_2 a1,n = 0 or ChangeVal_2 a1,n <> 0 ) ;

suppose A2: ChangeVal_2 a1,n = 0 ; :: thesis: a1 = a2

then ( a2 = 2 to_power n or a2 = 0 ) by A1, Def8;
hence a1 = a2 by A1, A2, Def8; :: thesis: verum

end;

suppose A3: ChangeVal_2 a1,n <> 0 ; :: thesis: a1 = a2

then A4: a1 <> 2 to_power n by Def8;
a2 <> 2 to_power n by A1, A3, Def8;
hence a2 = ChangeVal_2 a1,n by A1, Def8
.= a1 by A4, Def8 ;
:: thesis: verum

end;

end;