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:34;
hence ADD_MOD (i,j,n) is_expressible_by n by Def3; :: thesis: verum