One-Way property of Random Oracle I'm currently working on a proof in the Random Oracle model, and could not find the formal argument on why the random oracle is one-way (i.e. for an Oracle $O$, it is easy to calculate $x=O(n)$, but not efficiently possible to compute $n = O^{-1}(x)$).

Now, I know that the random oracle has that property, and it is intuitively obvious why (as the output is randomly chosen, it is independent from the input and does not contain any information about it). However, as it is not part of the formal specification of a random oracle as per Bellare and Rogaway (as far as I know), I'd like to know how you would formally prove it, based only on the formal specification of a random oracle.
This is very confusing because it seems as it should be something really easy to prove. However, it actually is not, and in fact the proof uses the Borel-Cantelli lemma. Anyway, it was formally proven by Rudich and Impagliazzo in their groundbreaking work on black-box separations. You can find a formal proof in Rudich's thesis, Section 6.2, or in the paper Limits on the provable consequences of one-way permutations by Impagliazzo and Rudich.