Every strict group object in Cat is a groupoid

Let $A$ and $O$ be arbitrary types equipped with group structures, and let $D$ consist of maps $s,t:A\to O$, $e:O\to A$, and a total function $c:A\times A\to A$, where $c(g,f)$ denotes the specified composition of $f$ followed by $g$; this function is defined even when $t(f)\ne s(g)$. Suppose these maps satisfy all the following conditions: for every $x\in O$, $s(e(x))=t(e(x))=x$; for every $f,g\in A$ with $t(f)=s(g)$, $s(c(g,f))=s(f)$ and $t(c(g,f))=t(g)$; for every $f\in A$, $c(e(t(f)),f)=f$ and $c(f,e(s(f)))=f$; and for every $f,g,k\in A$ with $t(f)=s(g)$ and $t(g)=s(k)$, $c(k,c(g,f))=c(c(k,g),f)$. Suppose also that multiplication preserves these maps: for every $a,b\in A$, $s(ab)=s(a)s(b)$ and $t(ab)=t(a)t(b)$; for every $x,y\in O$, $e(xy)=e(x)e(y)$; and for every $f,g,a,b\in A$ with $t(f)=s(g)$ and $t(a)=s(b)$, $c(gb,fa)=c(g,f)c(b,a)$. Assume further that $s(1_A)=t(1_A)=1_O$, $e(1_O)=1_A$, and $c(1_A,1_A)=1_A$. Finally, suppose inversion preserves the maps: for every $a\in A$, $s(a^{-1})=s(a)^{-1}$ and $t(a^{-1})=t(a)^{-1}$; for every $x\in O$, $e(x)^{-1}=e(x^{-1})$; and for every $f,g\in A$ with $t(f)=s(g)$, $c(g,f)^{-1}=c(g^{-1},f^{-1})$. Then for every $f\in A$ there exists $g\in A$ such that