Let 𝐺 =𝜋1(𝑋,𝑥0) and 𝐻 =𝜋1𝑝(𝜋1(˜𝑋,˜𝑥0)). Since 𝐻 is a subgroup its left cosets in 𝐻 are disjoint. Let 𝐴 be a set of loops 𝐴 ∋𝛼 :𝕀 →𝑋 with base 𝑥0, 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 ˜𝑥0.

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 ˜𝛽(1) =˜𝛼(1). Therefore Φ is well-defined.

For injectivity, let 𝛼,𝛽 ∈𝐴 such that ˜𝛼(1) =˜𝛽(1). It follows

so [𝛼] =[𝛽] ⊙[𝛽]−1 ⊙[𝛼] ∈[𝛽] ⊙𝐻 and thus [𝛼] ⊙𝐻 =[𝛽] ⊙𝐻. Thus 𝛼 =𝛽 by construction of 𝐴.

For surjectivity, let ˜𝑥′0 ∈𝑝−1{𝑥0} and let ˜𝛾 :𝕀 →˜𝑋 be a path from ˜𝑥0 to ˜𝑥′0. Then ˜𝛾 is the unique lift of a loop 𝛾 =𝑝 ∘˜𝛾 with basepoint 𝑥0, and therefore there exists some 𝛼 ∈𝐴 so that [𝛽] ∈[𝛼]𝐻, whence Φ[𝛼] =˜𝑥′0.

Define an equivalence relation ∼ on 𝑋, so that 𝑥 ∼𝑦 iff ∣𝑝−1{𝑥}∣ =∣𝑝−1{𝑦}∣. 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.