theorem proposition_25_6 {ι : Type u_1} (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), WeaklyLocallyCompactSpace (X i)] (U : (i : ι) → Set (X i)) (hU_open : ∀ (i : ι), IsOpen (U i)) (hU_compact : ∀ᶠ (i : ι) in Filter.cofinite, IsCompact (U i)) : WeaklyLocallyCompactSpace (RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite)