diff --git a/shelley/chain-and-ledger/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex
index 0cf4a914de8..6718a79a420 100644
--- a/shelley/chain-and-ledger/formal-spec/utxo.tex
+++ b/shelley/chain-and-ledger/formal-spec/utxo.tex
@@ -475,7 +475,7 @@ \subsection{Witnesses}
     \cup & ~~
            \{\fun{stakeCred_r}~a\mid a\mapsto \wcard \in \AddrRWDVKey
       \restrictdom \txwdrls{tx}\}\\
-    \cup & ~~\fun{certWitsNeeded}~{tx} \\
+    \cup & ~~(\AddrVKey \cap \fun{certWitsNeeded}~{tx}) \\
     \cup & ~~\fun{propWits}~(\fun{txup}~\var{tx})~\var{genDelegs} \\
     \cup & ~~\bigcup_{\substack{c \in \txcerts{tx} \\ ~c \in\DCertRegPool}} \fun{poolOwners}~{c}
   \end{align*}