Let X, Tx and U be given.

Assume H: partition_of_unity_dominated X Tx U.

Apply (partition_of_unity_dominated_ex_family_pred X Tx U H) to the current goal.

Let P be given.

Assume HP: partition_of_unity_family X Tx U P.

We use P to witness the existential quantifier.

An exact proof term for the current goal is (partition_of_unity_family_pointwise_finite_sum X Tx U P HP).

∎