The uniqueness of groups of type J₄

We give the first computer free proof of the uniqueness of groups of type J₄. In addition we supply simplified proofs of some properties of such groups, such as the structure of certain subgroups. A group of type J₄ is a finite group G possessing an involution z such that H=C_G(z) satisfies F*(H)=Q is extraspecial of order 2¹³, H/Q is isomorphic to Z₃ extended by Aut (M₂₂), and z^G ⋂ Q ≠ {z}. We prove: Main Theorem. Up to isomorphism there exists at most one group of type J₄.