Affine actions correspond to coordinate-ring coactions

Pull back an action along $a$ and apply F1. The two action identities evaluated on $f$ give respectively $f(ghx)=f(g(hx))$ and $f(ex)=f(x)$, precisely the displayed identities for $\delta$. Conversely F2 reconstructs a unique morphism from an algebra map $\delta$; F1 and equality of pullbacks turn the displayed identities back into the action identities. Thus this is a bijection, also for the empty $X$.

For this action define $b(x,g)=g^{-1}x$. Inversion is a morphism and $b(b(x,g),h)=h^{-1}{g}^{-1}x=(gh{)}^{-1}x=b(x,gh)$, while $b(x,e)=x$. Pullback gives exactly $c=\tau (S\otimes \mathrm{id})\delta$, with the right-comodule identities asserted. Conversely a right-comodule algebra map reconstructs $b$ by F2 and its identities by F1; $a(g,x)=b(x,g^{-1})$ reconstructs the original left action. This also proves that conversion of either coaction to the other is inverse, since inversion squared is the identity.

Evaluation gives $r(g)f(x)=f(g^{-1}x)$ and $r(g)r(h)f(x)=f(h^{-1}{g}^{-1}x)=r(gh)f(x)$, with $r(e)=\mathrm{id}$ and inverse $r(g^{-1})$. Finally $u(gx)=gu(x)$ is equivalent, by F2, to ${\delta }_X{u}^{\ast }=({\mathrm{id}}_H\otimes u^{\ast }){\delta }_Y$; conversion in step 2.1 gives the corresponding $c$ identity. AC is used only through F2, not through any selection of a vector-space basis.