Hopf problem: toric · diagonal quotient 4

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.DiagonalQuotient.fundamentalGroup_basepointChange_of_homotopy {F : Type u_1} {E : Type u_2} [TopologicalSpace F] [TopologicalSpace E] (f₀ f₁ : C(F, E)) (H : f₀.Homotopy f₁) (c : F) (v : FundamentalGroup F c) : (FundamentalGroup.fundamentalGroupMulEquivOfPath (H.evalAt c)) ((FundamentalGroup.map f₀ c) v) = (FundamentalGroup.map f₁ c) v