Let X, Tx, f and N be given.
Assume HTx: topology_on X Tx.
Assume HNTx: N ∈ Tx.
Assume Hdisj: support_of X Tx f ∩ N = Empty.
Let x be given.
Assume HxN: x ∈ N.
We will prove apply_fun f x = 0.
Apply (xm (apply_fun f x = 0)) to the current goal.
Assume Hx0: apply_fun f x = 0.
An exact proof term for the current goal is Hx0.
Assume Hxne0: ¬ (apply_fun f x = 0).
We prove the intermediate claim Hfx: apply_fun f x ≠ 0.
An exact proof term for the current goal is Hxne0.
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 HxX: x ∈ X.
An exact proof term for the current goal is (HNsubX x HxN).
We prove the intermediate claim HxSupp: x ∈ support_of X Tx f.
An exact proof term for the current goal is (support_of_contains_nonzero X Tx f x HTx HxX Hfx).
We prove the intermediate claim HxInt: x ∈ (support_of X Tx f ∩ N).
An exact proof term for the current goal is (binintersectI (support_of X Tx f) N x HxSupp HxN).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HxInt.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
∎