How can the identity $\textbf{Pr}[\textbf{y}=y|\textbf{x}=x] = \sum_{\lbrace K:x=d_K(y)\rbrace}\textbf{Pr}[\textbf{K}=K]$ be verified to hold? How can the identity $\textbf{Pr}[\textbf{y}=y|\textbf{x}=x] = \sum_{\lbrace K:x=d_K(y)\rbrace}\textbf{Pr}[\textbf{K}=K]$ be verified to hold for any cryptosystem?


In his book Cryptography, Theory and Practice (3rd edition), Stinson states the equality for $\textbf{Pr}[\textbf{x}=x|\textbf{y}=y]$, which can be seen in the snippet below.

Intuitively, this seems just fine... But given that $\textbf{Pr}[\textbf{x}=x|\textbf{y}=y] = \textbf{Pr}[\textbf{x}=x,\textbf{y}=y] / \textbf{Pr}[\textbf{y}=y]$ by definition, how can I verify that the claim does indeed hold for any cryptosystem?
The operation of the function is completely described by $P(X,Y,K)$ which factorizes as $P(Y|X,K)P(X)P(K)$ under the assumption that $X$ and $K$ are independent and leads to

$$P(Y) = \sum_X\sum_K P(Y|X,K)P(X)P(K)$$

If you restrict $X$ to only the particular one that $K$ maps onto $Y$ (by writing $X = D_k(y)$) then $P(Y|X,K) = 1$ under the assumption that the function is a bijection, then you end up with 

$$P(Y=y) = \sum_K P(K=k)P(X=D_k(y))$$

Using the same approach you can prove the conditional statement:

$$P(Y|X) = \sum_K P(Y|X,K)P(K) = \sum_K P(K)$$