let i, n be Element of NAT ; :: thesis: ( i is_expressible_by n implies ADD_MOD (0,i,n) = i )
assume i is_expressible_by n ; :: thesis: ADD_MOD (0,i,n) = i
then i < 2 to_power n by Def3;
hence ADD_MOD (0,i,n) = i by NAT_D:24; :: thesis: verum