Sweedler Notation: $\eta\epsilon$ is the identity element of the convolution product

Question

1. Proof attempt
   Let $(A, \mu, \eta) $ be an algebra and $(C, \Delta, \epsilon) $ be a coalgebra, both over the same field $k$.
   Define the convolution product $$*: \mathrm{Hom}(C,A)\otimes \mathrm{Hom}(C,A) \rightarrow \mathrm{Hom}(C,A); \qquad f \otimes g \mapsto \mu \circ (f \otimes g)\circ \Delta.$$ I saw (a less detailed version of) the following attempt to prove that $\eta \circ \epsilon$ is the identity element with respect to the convolution product: $$(f * (\eta \epsilon))(c)=\sum\limits_{(c)}f(c^{(1)})(\eta\epsilon)(c^{(2)})= \sum\limits_{(c)}f(c^{(1)})(\eta(\epsilon (c^{(2)})1_k)=\sum\limits_{(c)}f(c^{(1)})(\epsilon(c^{(2)})\eta(1_k))= \sum\limits_{(c)}f(c^{(1)})\epsilon(c^{(2)})=f(c).$$
2. Question
   

• Is that proof attempt correct?
• Specifically: The third step holds because of the linearity of the unit $\eta$; the fourth step due to the defining property of the unit (i.e. unitality); the last due to the defining property of the counit - correct?

Answer 1

Given that for every linear map $f$, it is often useful to write $A \otimes f$ and $f \otimes A$ instead of $Id_A \otimes f$ and $f \otimes Id_A$ respectively, my version of this proof is the following:

$$f * \eta\epsilon = \mu \circ (f \otimes \eta\epsilon) \circ \Delta = \mu \circ (A \otimes \eta) \circ (f\otimes \mathbb{k}) \circ (C \otimes \epsilon) \circ \Delta = r_A \circ (f\otimes \mathbb{k}) \circ (r_C)^{-1} = f$$ where $$r_A: A \otimes \mathbb{k} \rightarrow A\\ a\otimes k \mapsto ka$$

The second identity follows from a trick that's very usual in this type of proofs and it is verifiable by direct computation:

$$\mu \circ (f \otimes \eta\epsilon) \circ \Delta (c) = \sum f(c_1) \eta\epsilon(c_2)$$

while

$$\mu \circ (A \otimes \eta) \circ (f\otimes \mathbb{k}) \circ (C \otimes \epsilon) \circ \Delta (c) = \\ = \mu \circ (A \otimes \eta) \circ (f\otimes \mathbb{k}) (\sum c_1 \otimes \epsilon(c_2)) = \\ = \mu \circ (A \otimes \eta) (\sum f(c_1)\otimes \epsilon(c_2)) = \\ = \mu (\sum f(c_1)\otimes \eta\epsilon(c_2)) =\\ =\sum f(c_1) \eta\epsilon(c_2) $$