let i, n be Nat; :: thesis: ( i is_expressible_by n implies ( ChangeVal_1 (i,n) <= 2 to_power n & ChangeVal_1 (i,n) > 0 ) )
assume A1: i is_expressible_by n ; :: thesis: ( ChangeVal_1 (i,n) <= 2 to_power n & ChangeVal_1 (i,n) > 0 )
A2: 2 to_power n > 0 by POWER:34;

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: ( ChangeVal_1 (i,n) <= 2 to_power n & ChangeVal_1 (i,n) > 0 )

hence ( ChangeVal_1 (i,n) <= 2 to_power n & ChangeVal_1 (i,n) > 0 ) by A2, Def7; :: thesis: verum

end;

suppose A3: i <> 0 ; :: thesis: ( ChangeVal_1 (i,n) <= 2 to_power n & ChangeVal_1 (i,n) > 0 )

then ChangeVal_1 (i,n) = i by Def7;
hence ( ChangeVal_1 (i,n) <= 2 to_power n & ChangeVal_1 (i,n) > 0 ) by A1, A3; :: thesis: verum

end;

end;