let i, n be Element of 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:39;

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, Def3; :: thesis: verum

end;

end;