let i, n be Element of NAT ; :: thesis: ( i is_expressible_by n implies ChangeVal_2 (i,n) is_expressible_by n )
assume i is_expressible_by n ; :: thesis: ChangeVal_2 (i,n) is_expressible_by n
then i < 2 to_power n by Def3;
then ChangeVal_2 (i,n) < 2 to_power n by Def8;
hence ChangeVal_2 (i,n) is_expressible_by n by Def3; :: thesis: verum