∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ},
  1 ≤ r →
    Meromorphic f₁ →
      (∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) →
        Meromorphic f₂ →
          (∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) →
            ValueDistribution.logCounting (f₁ * f₂) ⊤ r ≤
              (ValueDistribution.logCounting f₁ ⊤ + ValueDistribution.logCounting f₂ ⊤) r