Let X, Tx, f and g be given.
Assume HTx: topology_on X Tx.
Assume HfR: ∀x : set, x ∈ X → apply_fun f x ∈ R.
Assume HgR: ∀x : set, x ∈ X → apply_fun g x ∈ R.
We will prove support_of X Tx (compose_fun X (pair_map X f g) mul_fun_R) ⊆ support_of X Tx g.
Set h to be the term compose_fun X (pair_map X f g) mul_fun_R.
Set nz_h to be the term {x ∈ X|apply_fun h x ≠ 0}.
Set nz_g to be the term {x ∈ X|apply_fun g x ≠ 0}.
We prove the intermediate claim Hnz_h_sub: nz_h ⊆ nz_g.
Let x be given.
Assume Hx: x ∈ nz_h.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun h x0 ≠ 0) x Hx).
We prove the intermediate claim Hhxne0: apply_fun h x ≠ 0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun h x0 ≠ 0) x Hx).
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (HfR x HxX).
We prove the intermediate claim HgxR: apply_fun g x ∈ R.
An exact proof term for the current goal is (HgR x HxX).
We prove the intermediate claim Hhx: apply_fun h x = mul_SNo (apply_fun f x) (apply_fun g x).
An exact proof term for the current goal is (mul_of_pair_map_apply X f g x HxX HfxR HgxR).
We prove the intermediate claim Hgneq0: apply_fun g x ≠ 0.
Assume Hg0: apply_fun g x = 0.
We prove the intermediate claim HfxS: SNo (apply_fun f x).
An exact proof term for the current goal is (real_SNo (apply_fun f x) HfxR).
We prove the intermediate claim HgxS: SNo (apply_fun g x).
An exact proof term for the current goal is (real_SNo (apply_fun g x) HgxR).
We prove the intermediate claim Hmul0: mul_SNo (apply_fun f x) (apply_fun g x) = 0.
rewrite the current goal using Hg0 (from left to right).
An exact proof term for the current goal is (mul_SNo_zeroR (apply_fun f x) HfxS).
We prove the intermediate claim Hh0: apply_fun h x = 0.
rewrite the current goal using Hhx (from left to right).
An exact proof term for the current goal is Hmul0.
An exact proof term for the current goal is (Hhxne0 Hh0).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun g x0 ≠ 0) x HxX Hgneq0).
We prove the intermediate claim Hnz_g_subX: nz_g ⊆ X.
Let x be given.
Assume Hx: x ∈ nz_g.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun g x0 ≠ 0) x Hx).
We prove the intermediate claim Hcl_sub: closure_of X Tx nz_h ⊆ closure_of X Tx nz_g.
An exact proof term for the current goal is (closure_monotone X Tx nz_h nz_g HTx Hnz_h_sub Hnz_g_subX).
Let x be given.
Assume Hx: x ∈ support_of X Tx h.
We will prove x ∈ support_of X Tx g.
We prove the intermediate claim Hdef_h: support_of X Tx h = closure_of X Tx nz_h.
Use reflexivity.
We prove the intermediate claim Hdef_g: support_of X Tx g = closure_of X Tx nz_g.
Use reflexivity.
We prove the intermediate claim Hxclh: x ∈ closure_of X Tx nz_h.
rewrite the current goal using Hdef_h (from right to left).
An exact proof term for the current goal is Hx.
We prove the intermediate claim Hxcl: x ∈ closure_of X Tx nz_g.
An exact proof term for the current goal is (Hcl_sub x Hxclh).
rewrite the current goal using Hdef_g (from left to right).
An exact proof term for the current goal is Hxcl.
∎