Internal Grp categories correspond to group objects in Cat

For arbitrary groups $A,O$ and total maps $s,t:A\to O$, $i:O\to A$, and $c:A\times A\to A$, the theorem asserts an equivalence between two conditions described as follows. Let $\mathcal C$ mean the conjunction of $s(i(x))=t(i(x))=x$ for every $x\in O$; $s(c(g,f))=s(f)$ and $t(c(g,f))=t(g)$ whenever $t(f)=s(g)$; $c(i(t(f)),f)=f$ and $c(f,i(s(f)))=f$ for every $f\in A$; and $c(h,c(g,f))=c(c(h,g),f)$ whenever $t(f)=s(g)$ and $t(g)=s(h)$. Let $\mathcal H$ mean the conjunction of $s(1_A)=t(1_A)=1_O$, $s(ab)=s(a)s(b)$ and $t(ab)=t(a)t(b)$ for every $a,b\in A$, $i(1_O)=1_A$, $i(xy)=i(x)i(y)$ for every $x,y\in O$, $c(1_A,1_A)=1_A$, and $c(gb,fa)=c(g,f)c(b,a)$ for every $f,g,a,b\in A$ satisfying $t(f)=s(g)$ and $t(a)=s(b)$. The first condition is $\mathcal C\land\mathcal H$. The second condition is $\mathcal C\land\mathcal H$ together with $s(a^{-1})=s(a)^{-1}$ and $t(a^{-1})=t(a)^{-1}$ for every $a\in A$, $i(x)^{-1}=i(x^{-1})$ for every $x\in O$, and $c(g,f)^{-1}=c(g^{-1},f^{-1})$ for every $f,g\in A$ with $t(f)=s(g)$. These two conditions are equivalent, with no further assumptions on the total composition map outside the cases constrained by the listed equations.