[proofplan] We first show that the union of the generic filter is a function: directedness of the filter makes any two conditions in $G$ compatible, so they cannot assign different values to the same integer. We then prove totality by meeting, for each $n \in \omega$, the dense set of conditions that decide the value at $n$. Finally, we compute the valuation of the canonical name $\dot{c}$ directly from its definition and identify it with the graph of the function $c$. [/proofplan] [step:Use directedness of the filter to make the union single valued] Let $\mathbb{P}:=\operatorname{Add}(\omega,1)$. Each condition $p \in \mathbb{P}$ is a finite partial function $p:\omega \rightharpoonup 2$. Define the relation $c \subset \omega \times 2$ by \begin{align*} c = \bigcup_{p \in G} p. \end{align*} We prove that $c$ is single valued. Suppose $n \in \omega$, $i,j \in 2$, and $(n,i),(n,j) \in c$. By the definition of union, there exist conditions $p,q \in G$ such that $p(n)=i$ and $q(n)=j$. Since $G$ is a filter, it is directed: there exists $r \in G$ such that $r \le p$ and $r \le q$. The order on $\mathbb{P}$ is reverse inclusion, so $r \supset p$ and $r \supset q$. Hence $r(n)=p(n)=i$ and $r(n)=q(n)=j$. Since $r$ is a function, $i=j$. Therefore $c$ is a function on its domain. [guided] Let $\mathbb{P}:=\operatorname{Add}(\omega,1)$. A condition $p \in \mathbb{P}$ is a finite partial function $p:\omega \rightharpoonup 2$, and the ordering is reverse inclusion: a stronger condition contains more decided bits. We define the candidate real as the union of all conditions in the generic filter: \begin{align*} c = \bigcup_{p \in G} p. \end{align*} The only possible obstruction to $c$ being a function is disagreement: two different conditions in $G$ might assign different values to the same integer. We rule this out using the filter property. Suppose $n \in \omega$ and $i,j \in 2$ satisfy $(n,i),(n,j) \in c$. Then there are conditions $p,q \in G$ with $p(n)=i$ and $q(n)=j$. Because $G$ is a filter, it is directed. Therefore there exists $r \in G$ with $r \le p$ and $r \le q$. Since the order is reverse inclusion, this means $r \supset p$ and $r \supset q$. Thus $r$ extends both partial functions. In particular, \begin{align*} r(n)=p(n)=i. \end{align*} Also, \begin{align*} r(n)=q(n)=j. \end{align*} Since $r$ is itself a function, it cannot assign two different values to $n$. Hence $i=j$. This proves that the union $c$ is single valued, so $c$ is a function from its domain into $2$. [/guided] [/step] [step:Meet the dense set of conditions deciding each coordinate] Fix $n \in \omega$. Define \begin{align*} D_n := \{p \in \mathbb{P} : n \in \operatorname{dom}(p)\}. \end{align*} We show that $D_n$ is dense in $\mathbb{P}$. Let $p \in \mathbb{P}$. If $n \in \operatorname{dom}(p)$, then $p \in D_n$. If $n \notin \operatorname{dom}(p)$, define the finite partial function $q:\omega \rightharpoonup 2$ by \begin{align*} q := p \cup \{(n,0)\}. \end{align*} Then $q \in \mathbb{P}$, $q \le p$, and $q \in D_n$. Thus $D_n$ is dense. Since $G$ is generic, $G \cap D_n \neq \varnothing$. Choose $p_n \in G \cap D_n$. Then $n \in \operatorname{dom}(p_n)$, so $(n,p_n(n)) \in c$. Since $n \in \omega$ was arbitrary and the previous step showed that $c$ is single valued, $c:\omega \to 2$ is a total function. [/step] [step:Evaluate the canonical Cohen name as the graph of the union] By the definition of valuation of a forcing name by a generic filter, \begin{align*} (\dot{c})_G = \{x : \text{there exists } p \in G \text{ such that } (\check{x},p) \in \dot{c}\}. \end{align*} Let $x$ be any set. From the definition of $\dot{c}$, membership $x \in (\dot{c})_G$ holds exactly when there exist $p \in G$, $n \in \omega$, and $i \in 2$ such that $x=(n,i)$, $n \in \operatorname{dom}(p)$, and $i=p(n)$. Since $p \subset c$, this implies $i=c(n)$, so \begin{align*} (\dot{c})_G \subset \{(n,c(n)) : n \in \omega\}. \end{align*} Conversely, fix $n \in \omega$. Since $c:\omega \to 2$ is total, there exists $p \in G$ such that $n \in \operatorname{dom}(p)$ and $p(n)=c(n)$. Therefore $(\check{(n,c(n))},p) \in \dot{c}$, and hence $(n,c(n)) \in (\dot{c})_G$. Thus \begin{align*} \{(n,c(n)) : n \in \omega\} \subset (\dot{c})_G. \end{align*} The two inclusions give \begin{align*} (\dot{c})_G = \{(n,c(n)) : n \in \omega\}. \end{align*} This proves both claims. [/step]