Without loss of generality we may assume 𝑓0(0) =𝑓1(0) =1, since 𝑓0 ≃𝑓0(1)−1𝑓0 and has the same degree. First we will show that 𝐹 :𝑓0 ≃𝑓1 implies deg⁡𝑓0 =deg⁡𝑓1. Let 𝑓𝑠(𝑥) =𝐹(𝑥,𝑠), where we may assume without loss of generality that 𝑓𝑡(1) =1. Let 𝜑𝑠 :[0,1] →ℝ be the uniquely defined morphism for each 𝑠 ∈[0,1] with 𝜑𝑠(0) =0 and 𝑓𝑠ex =ex⁡𝜑𝑠. Since 𝑓−ex :[0,1] ×[0,1] →𝕊1 is continuous and thus uniformly continuous by the Heine-Cantor theorem, we can divide [0,1] by 0 =𝑡0 <𝑡1 <⋯ <𝑡𝑘 =1 with finite 𝑘 so that for all 𝑠 ∈[0,1]

for all integers 0 ≤𝑗(𝑡) ≤𝑘 −1. As in the proof of this theorem, we define 𝜑𝑠 as follows

which is continuous by properties of the Main branch of the complex logarithm. Then Φ :[0,1] ×[0,1] →ℝ :(𝑥,𝑡) ↦𝜑𝑡(𝑥) is continuous, and thus a constant map since it is always an integer. Herefore

as required. For the converse, let deg⁡𝑓0 =deg⁡𝑓1. Then let 𝜑𝑘 be the uniquely defined morphisms with 𝜑𝑘(0) =0 and 𝑓𝑘ex =ex⁡𝜑𝑘 for 𝑘 ∈{0,1}. We may extend this to 𝑠 ∈[0,1] by

which has the property that 𝜑𝑠(1) =𝜑0(1) =𝜑1(1) ∈ℤ for all 𝑠 ∈[0,1]. Then ex⁡𝜑𝑠(1) =1 =ex⁡𝜑𝑠(1) for all 𝑠 ∈[0,1]. Note that ex ×id :[0,1] ×[0,1] →𝕊1 ×[0,1] is just the natural projection for the quotient topology, and thus by its universal property there exists a unique continuous 𝐻 :𝕊 ×[0,1] →𝕊1 such that 𝐻 ∘(ex ×id) =ex ∘Φ. This unique 𝐻 defines a homotopy 𝑓0 ≃𝑓1, since

for all 𝑘 ∈{0,1} and ex is a monomorphism, implying 𝐻(𝑡,𝑘) =𝑓𝑘(𝑡) as required.