Normalization of a finite nonnegative weight

For every universe-level-0 type $Ω$ equipped with a finite enumeration and every real-valued function $w$ on $Ω$, if $w(ω)≥0$ for every $ω∈Ω$ and there exists an $ω∈Ω$ with $w(ω)>0$, then the finite sum $Z=Σ_{ω∈Ω}w(ω)$ is strictly positive, and the function $ω↦w(ω)/Z$ is a probability weight in the exact sense that it is nonnegative at every $ω$ and its finite sum is exactly $1$. There is no separate nonemptiness assumption: the existential strict-positivity hypothesis forces a witness when it is satisfiable; for an empty type, or for a weight having no strictly positive value, the theorem's implication is vacuous.