Let X, Tx, P, N, F0 and f be given.
Assume HTx: topology_on X Tx.
Assume HNTx: N ∈ Tx.
Assume HF0subP: F0 ⊆ P.
Assume Hctrl: ∀g : set, g ∈ P → support_of X Tx g ∩ N ≠ Empty → g ∈ F0.
Assume HfP: f ∈ P.
Assume HnotF0: ¬ (f ∈ F0).
Let x be given.
Assume HxN: x ∈ N.
We will prove apply_fun f x = 0.
We prove the intermediate claim Hdisj: support_of X Tx f ∩ N = Empty.
Apply (xm (support_of X Tx f ∩ N = Empty)) to the current goal.
Assume H: support_of X Tx f ∩ N = Empty.
An exact proof term for the current goal is H.
Assume Hne: ¬ (support_of X Tx f ∩ N = Empty).
We prove the intermediate claim Hmeet: support_of X Tx f ∩ N ≠ Empty.
An exact proof term for the current goal is Hne.
We prove the intermediate claim HfF0: f ∈ F0.
An exact proof term for the current goal is (Hctrl f HfP Hmeet).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotF0 HfF0).
An exact proof term for the current goal is (support_disjoint_open_implies_zero_on_open X Tx f N HTx HNTx Hdisj x HxN).
∎