[proofplan] We first verify that the codomain of $\tilde f$ is correct: every value $f(a)$ belongs to $\operatorname{im} f$ by the defining property of the image. Surjectivity is then immediate from the same definition, because an arbitrary element of $\operatorname{im} f$ is, by definition, equal to $f(a)$ for some $a \in A$. Finally, we compare $f$ and $\iota \circ \tilde f$ pointwise on $A$, using that $\iota$ is the inclusion map. [/proofplan] [step:Verify that $\tilde f$ is well-defined as a map into $\operatorname{im} f$] Let $a \in A$ be arbitrary. By the definition of $\operatorname{im} f$, the element $f(a) \in B$ belongs to $\operatorname{im} f$, with $a$ itself serving as a witness. Hence the rule $a \mapsto f(a)$ indeed defines a function \begin{align*} \tilde f: A \to \operatorname{im} f. \end{align*} [guided] The only point that needs checking in the definition of $\tilde f$ is its codomain. The original function is \begin{align*} f: A \to B, \end{align*} so for every $a \in A$ we know that $f(a) \in B$. But $\tilde f$ is declared to have codomain $\operatorname{im} f$, which is the subset of $B$ consisting exactly of those elements of the form $f(x)$ for some $x \in A$. Fix $a \in A$. To prove that $f(a) \in \operatorname{im} f$, we must exhibit an element of $A$ whose image under $f$ is $f(a)$. The element $a$ itself does this, since \begin{align*} f(a)=f(a). \end{align*} Therefore $f(a) \in \operatorname{im} f$. Since this holds for every $a \in A$, the formula $\tilde f(a)=f(a)$ defines a genuine function \begin{align*} \tilde f: A \to \operatorname{im} f. \end{align*} [/guided] [/step] [step:Prove that every element of $\operatorname{im} f$ is hit by $\tilde f$] Let $y \in \operatorname{im} f$. By the definition of $\operatorname{im} f$, there exists $a \in A$ such that \begin{align*} f(a)=y. \end{align*} For this element $a$, the definition of $\tilde f$ gives \begin{align*} \tilde f(a)=f(a)=y. \end{align*} Thus every $y \in \operatorname{im} f$ has a preimage under $\tilde f$, so $\tilde f$ is surjective. [/step] [step:Compute the composition pointwise on $A$] Let $a \in A$. Since $\tilde f(a) \in \operatorname{im} f$, the value $\iota(\tilde f(a))$ is defined. Using the definition of composition, the definition of $\tilde f$, and the fact that $\iota$ is the inclusion map, we obtain \begin{align*} (\iota \circ \tilde f)(a)=\iota(\tilde f(a))=\iota(f(a))=f(a). \end{align*} Therefore $f$ and $\iota \circ \tilde f$ agree at every element of $A$. [/step] [step:Conclude equality of the two functions] Both $f$ and $\iota \circ \tilde f$ are functions from $A$ to $B$. The preceding step proves that for every $a \in A$, \begin{align*} (\iota \circ \tilde f)(a)=f(a). \end{align*} By equality of functions with the same domain and codomain, it follows that \begin{align*} f = \iota \circ \tilde f. \end{align*} Together with the surjectivity of $\tilde f$, this proves the theorem. [/step]