∀ {𝕂 : Type u_1} (𝔸 : Type u_2) [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a a_1 : 𝕂),
  a = a_1 →
    ∀ (b b_1 : 𝕂),
      b = b_1 →
        ∀ (c c_1 : 𝕂),
          c = c_1 → ∀ (n : ℕ), ordinaryHypergeometricSeries 𝔸 a b c n = ordinaryHypergeometricSeries 𝔸 a_1 b_1 c_1 n