∀ {F : Type u_1} {α : outParam (Type u_2)} [inst : Ring α] [inst_1 : FunLike F α ℝ] [RingSeminormClass F α ℝ] {f g : F},
  IsPowMul ⇑f →
    IsPowMul ⇑g →
      (∃ r, ∃ (_ : 0 < r), ∀ (a : α), f a ≤ r * g a) → (∃ r, ∃ (_ : 0 < r), ∀ (a : α), g a ≤ r * f a) → f = g