A connected graded bialgebra has a unique antipode, given by the reduced-coproduct recursion

If $x\in H_n$ with $n>0$, gradedness places $\mathrm{\Delta }(x)$ in ${⨁}_{i+j=n}{H}_i{\otimes }_k{H}_j$. Since $\epsilon$ vanishes in positive degree and $H_0=k{1}_H$, the two counit identities force the bidegree $(0,n)$ and $(n,0)$ components to be $1_H\otimes x$ and $x\otimes 1_H$. Hence $\tilde{\mathrm{\Delta }}(x)\in {⨁}_{i=1}^{n-1}{H}_i{\otimes }_k{H}_{n-i}$, with $\tilde{\mathrm{\Delta }}(x)=0$ when $n=1$; for $c\in k$, $\mathrm{\Delta }(u(c))=u(c)\otimes 1_H$ and $\epsilon (u(c))=c$.

For $f,g,h\in {\mathrm{Hom}}_k(H,H)$, the convolution bracketings are $(f\ast g)\ast h=m(m\otimes \mathrm{i}\mathrm{d})(f\otimes g\otimes h)(\mathrm{\Delta }\otimes \mathrm{i}\mathrm{d})\mathrm{\Delta }$ and $f\ast (g\ast h)=m(\mathrm{i}\mathrm{d}\otimes m)(f\otimes g\otimes h)(\mathrm{i}\mathrm{d}\otimes \mathrm{\Delta })\mathrm{\Delta }$. Under the canonical rebracketing [F4], coassociativity of $\mathrm{\Delta }$ and associativity of $m$ identify these maps. Hence convolution is associative, and its unit is $e:=u\epsilon$ by [F5].

Set $S_{\mathrm{\ell }}{\mathrm{\mid }}_{H_0}=S_r{\mathrm{\mid }}_{H_0}={\mathrm{i}\mathrm{d}}_{H_0}$. Inductively, once both maps are defined on ${⨁}_{j<n}{H}_j$, define for $x\in H_n$ by $S_{\mathrm{\ell }}(x):=-x-m(S_{\mathrm{\ell },<n}\otimes \mathrm{i}\mathrm{d})\tilde{\mathrm{\Delta }}(x)$ and $S_r(x):=-x-m(\mathrm{i}\mathrm{d}\otimes S_{r,<n})\tilde{\mathrm{\Delta }}(x)$, where $S_{\mathrm{\ell },<n}$ and $S_{r,<n}$ are their restrictions to ${⨁}_{j<n}{H}_j$. By step 1.1 both tensor factors of $\tilde{\mathrm{\Delta }}(x)$ have degree below $n$, so [F3] makes the displayed maps well defined on the tensor element itself, independently of any chosen finite expression as elementary tensors; they are $k$-linear in $x$ and extend to $H_n$. Induction over $n$ therefore defines $k$-linear maps $S_{\mathrm{\ell }},S_r:H\to H$.

For homogeneous $x\in H_n$ with $n>0$, step 2.1 gives $m(S_{\mathrm{\ell }}\otimes \mathrm{i}\mathrm{d})\mathrm{\Delta }(x)=S_{\mathrm{\ell }}(x)+x+m(S_{\mathrm{\ell },<n}\otimes \mathrm{i}\mathrm{d})\tilde{\mathrm{\Delta }}(x)=0=u\epsilon (x)$. For $x=u(c)\in H_0$, $S_{\mathrm{\ell }}$ is the identity and $\mathrm{\Delta }(u(c))=u(c)\otimes 1_H$, so the same convolution identity equals $u\epsilon (x)$. By linearity, $S_{\mathrm{\ell }}\ast \mathrm{i}\mathrm{d}=u\epsilon$ on $H$.

For homogeneous $x\in H_n$ with $n>0$, the right recursion in step 2.1 gives $m(\mathrm{i}\mathrm{d}\otimes S_r)\mathrm{\Delta }(x)=x+S_r(x)+m(\mathrm{i}\mathrm{d}\otimes S_{r,<n})\tilde{\mathrm{\Delta }}(x)=0=u\epsilon (x)$. The identity holds on $H_0$ because $S_r{\mathrm{\mid }}_{H_0}={\mathrm{i}\mathrm{d}}_{H_0}$ and $\mathrm{\Delta }(u(c))=u(c)\otimes 1_H$. Thus $\mathrm{i}\mathrm{d}\ast S_r=u\epsilon$ on all of $H$.

By steps 3.1 and 3.2, $S_{\mathrm{\ell }}\ast \mathrm{i}\mathrm{d}=e=\mathrm{i}\mathrm{d}\ast S_r$. Associativity and the unit from step 1.2 yield $S_{\mathrm{\ell }}=S_{\mathrm{\ell }}\ast e=S_{\mathrm{\ell }}\ast (\mathrm{i}\mathrm{d}\ast S_r)=(S_{\mathrm{\ell }}\ast \mathrm{i}\mathrm{d})\ast S_r=e\ast S_r=S_r$. Their common value $S$ is therefore a two-sided convolution inverse of $\mathrm{i}\mathrm{d}$, so it satisfies both displayed antipode identities.

If $T$ is any other antipode, then $T\ast \mathrm{i}\mathrm{d}=e=\mathrm{i}\mathrm{d}\ast S$. Associativity and the unit imply $T=T\ast e=T\ast (\mathrm{i}\mathrm{d}\ast S)=(T\ast \mathrm{i}\mathrm{d})\ast S=e\ast S=S$, so the antipode is unique.

The recursion preserves degree: if $x\in H_n$, step 1.1 places every reduced-coproduct term in $H_i\otimes H_{n-i}$ with $1\le i<n$; induction gives $S(H_i)\subseteq H_i$, and the graded multiplication then puts every recursive product in $H_n$. The base case is $S{\mathrm{\mid }}_{H_0}=\mathrm{i}\mathrm{d}$. The construction uses induction on $n$ and canonical maps on $\tilde{\mathrm{\Delta }}(x)$, never selected tensor representatives; thus no form of the axiom of choice is used. This proves the graded antipode claim.