The sequences are assumed to be bounded!
I suspect it is, since $\varliminf a_n + \varlimsup b_n \leq \varlimsup (a_n+b_n)$ is. But I have not managed to prove it.
I thought it possible to mirror the following trick when proving the inequality for sums:
$\varlimsup b_n = \varlimsup (a_n + b_n - a_n) \leq \varlimsup (a_n + b_n ) + \varlimsup(-a_n) = \varlimsup (a_n + b_n ) -\varliminf(a_n)$
But the incipient idea fell short rather fast:
$0 = \varlimsup (a_n b_n - a_n b_n) \leq \varlimsup (a_n b_n) + \varlimsup (-a_n b_n)$
I was hoping to manipulate $\varlimsup (-a_n b_n)$ in some ingenious way, but have not succeded.
Would love to read any ideas or hints.
Under the assumption that the sequences $(a_n)$ and $(b_n)$ are bounded:
Let $\alpha = \liminf a_n$ and $\beta = \limsup b_n$ (the boundedness assumption telling us that $-\infty < \alpha,\beta < \infty)$. Let $\epsilon > 0$. By definitions, we know that $a_n > \alpha - \epsilon$ for all $n$ sufficiently large and that $b_n > \beta - \epsilon$ for infinitely many $n$. Therefore also $a_n b_n > (\alpha - \epsilon)(\beta - \epsilon) = \alpha\beta - \epsilon(\alpha+\beta) + \epsilon^2$ for infinitely many $n$. This implies that $\limsup (a_n b_n) > \alpha\beta - \epsilon(\alpha+\beta) + \epsilon^2$. This holds for arbitrary $\epsilon$, so we conclude $\limsup(a_n b_n) \geq \alpha \beta$ as desired.
If either of the sequences is not bounded, there may be some other cases to check, but I am a bit too lazy to check them all :)