I’ve proved today the theorem:
Theorem Monovalued reloids are metamonovalued.
In other words:
Theorem if is a monovalued reloid and is a set of reloids (with matching sources and destination).
The proof uses the lemma, which is a special case (when is a principal reloid) of the theorem. The proof is now presented in the preprint of my book.