Uniqueness up to equivalence follows from equivalence of coverings criterion. Since is semilocally simply connected, it has a universal covering . Let According to Deck transformation group of a regular covering as quotient

is an isomorphism, where is the unique lift of with , and denotes a unique deck transformation with this property.

Now take the orbit space with the canonical projection

Since the deck transformation group acts properly discontinuously, so too does , and the orbit space of a properly discontinuous effective group action forms a covering, which in this case is universal. Thus

We now define

which is well-defined since iff for some , and then ; and continuous by Universal property.

Now let and let be a neighbourhood of evenly covered by with sheets . Let such that for all there exists exactly one such that , and let . Then

and , therefore is a covering. Then by construction

so as required.