Let and . Since is a subgroup its left cosets in are disjoint. Let be a set of loops with base , each a representative of a different left coset so that

and thus . We claim the map

is injective, where is the unique lift of based at .

To show this map is independent of choice of representative, let be a loop such that . Then where . Letting , , be the lifts of respectively, it follows that , and in particular . Therefore is well-defined.

For injectivity, let such that . It follows

so and thus . Thus by construction of .

For surjectivity, let and let be a path from to . Then is the unique lift of a loop with basepoint , and therefore there exists some so that , whence .

Define an equivalence relation on , so that iff . The equivalence classes are then unions of evenly covered open sets and hence open. But is the discrete union of these equivalence classes, so since is connected there can only be one equivalence class.