Let X, Tx, P, N and F0 be given.

Assume HTx: topology_on X Tx.

Assume HNTx: N ∈ Tx.

Assume HF0fin: finite F0.

Assume HF0sub: F0 ⊆ P.

Assume Hctrl: ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0.

Let y be given.

Assume HyN: y ∈ N.

Let f be given.

Assume HfP: f ∈ P.

Assume Hfy: apply_fun f y ≠ 0.

We will prove f ∈ F0.

We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.

An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).

We prove the intermediate claim HNPow: N ∈ 𝒫 X.

An exact proof term for the current goal is (HTsub N HNTx).

We prove the intermediate claim HNsubX: N ⊆ X.

An exact proof term for the current goal is (PowerE X N HNPow).

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (HNsubX y HyN).

We prove the intermediate claim HySupp: y ∈ support_of X Tx f.

An exact proof term for the current goal is (support_of_contains_nonzero X Tx f y HTx HyX Hfy).

We prove the intermediate claim Hmeet: support_of X Tx f ∩ N ≠ Empty.

Assume Hempty: support_of X Tx f ∩ N = Empty.

We prove the intermediate claim HyInt: y ∈ support_of X Tx f ∩ N.

An exact proof term for the current goal is (binintersectI (support_of X Tx f) N y HySupp HyN).

We prove the intermediate claim HyE: y ∈ Empty.

rewrite the current goal using Hempty (from right to left).

An exact proof term for the current goal is HyInt.

An exact proof term for the current goal is (EmptyE y HyE).

An exact proof term for the current goal is (Hctrl f HfP Hmeet).

∎