let i, j, n be Element of NAT ; :: thesis: ADD_MOD i,j,n is_expressible_by n
ADD_MOD i,j,n < 2 to_power n by NAT_D:1, POWER:39;
hence ADD_MOD i,j,n is_expressible_by n by Def3; :: thesis: verum