[proofplan] The proof is obtained by unfolding the definition of the image of a function. Membership in $\operatorname{im} f$ means precisely that the element is equal to $f(a)$ for at least one input $a \in A$. We prove the two implications separately: first extracting such a witness from membership in the image, and then using a given witness to prove membership in the image. [/proofplan] [step:Unfold the definition of the image] By definition, the image of the function $f: A \to B$ is the subset of $B$ given by \begin{align*} \operatorname{im} f = \{f(a) \in B : a \in A\}. \end{align*} Equivalently, for an element $b \in B$, the assertion $b \in \operatorname{im} f$ means that there exists an element $a \in A$ such that $b=f(a)$. [guided] The only definition needed is the definition of the image of a function. Since $f: A \to B$ is a function, every value $f(a)$ with $a \in A$ lies in $B$. The image records exactly all such values: \begin{align*} \operatorname{im} f = \{f(a) \in B : a \in A\}. \end{align*} Therefore, saying that a fixed element $b \in B$ belongs to $\operatorname{im} f$ is the same as saying that $b$ is one of the values taken by $f$. In quantified form, this means that there exists some $a \in A$ such that $b=f(a)$. [/guided] [/step] [step:Prove both implications from the unfolded definition] Fix $b \in B$. First suppose that $b \in \operatorname{im} f$. By the definition of $\operatorname{im} f$, there exists $a \in A$ such that $b=f(a)$. By symmetry of equality, $f(a)=b$. Hence \begin{align*} \exists a \in A \text{ such that } f(a)=b. \end{align*} Conversely, suppose that there exists $a \in A$ such that $f(a)=b$. Since $a \in A$, the value $f(a)$ belongs to $\operatorname{im} f$ by definition of the image. Since $f(a)=b$, substituting equal elements gives $b \in \operatorname{im} f$. Thus, for every $b \in B$, \begin{align*} b \in \operatorname{im} f \iff \exists a \in A \text{ such that } f(a)=b. \end{align*} [/step]