let n, a1, a2 be Nat; :: thesis: ( a1 <> 0 & a2 <> 0 & ChangeVal_2 (a1,n) = ChangeVal_2 (a2,n) implies a1 = a2 )
assume that
A1: ( a1 <> 0 & a2 <> 0 ) and
A2: 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 A3: ChangeVal_2 (a1,n) = 0 ; :: thesis: a1 = a2

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

end;

suppose A4: ChangeVal_2 (a1,n) <> 0 ; :: thesis: a1 = a2

then A5: a1 <> 2 to_power n by Def8;
a2 <> 2 to_power n by A2, A4, Def8;
hence a2 = ChangeVal_2 (a1,n) by A2, Def8
.= a1 by A5, Def8 ;
:: thesis: verum

end;

end;