A useful comodule natural transformation formula determines from a single linear functional. Define
using the regular right comodule . For any vector space , the cofree right comodule has coaction . Naturality with respect to all maps gives
The coaction is itself a morphism of right comodules. Its naturality equation, followed by , therefore gives
This derivation works for all comodules, not merely finite-dimensional ones.
The monoidal equation , evaluated on the two regular comodules and followed by their counits, implies
The unit equation gives . Thus is a unital algebra homomorphism over a field . In addition, the -colinearity of gives the useful intertwining relation
This fixes the orientation of relative to .
For the convolution product for coalgebra maps, define . Multiplicativity of and the two antipode identities show
Consequently
Coassociativity and the two convolution identities verify both composites directly. Since was a -comodule morphism, its linear inverse is also a -comodule morphism. Inverting the naturality and monoidal equations shows that the inverses form a monoidal natural transformation . Every such monoidal transformation is therefore invertible, without requiring a bijective antipode.