∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X),
  (f.toPartitionOfUnity i) x = (f i) x * ∏ᶠ (j : ι) (_ : WellOrderingRel j i), (1 - (f j) x)