∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : AddCommMonoid β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ : ι → α → β}, (∀ (i : ι), 0 ≤ h₁ i (f i)) → 0 ≤ f.sum h₁