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 f.
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_f to be the term {x ∈ X|apply_fun f x ≠ 0}.
We prove the intermediate claim Hnz_h_sub: nz_h ⊆ nz_f.
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 Hfne0: apply_fun f x ≠ 0.
Assume Hf0: apply_fun f x = 0.
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 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 Hmul0: mul_SNo (apply_fun f x) (apply_fun g x) = 0.
rewrite the current goal using Hf0 (from left to right).
An exact proof term for the current goal is (mul_SNo_zeroL (apply_fun g x) HgxS).
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 f x0 ≠ 0) x HxX Hfne0).
We prove the intermediate claim Hnz_f_subX: nz_f ⊆ X.
Let x be given.
Assume Hx: x ∈ nz_f.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ≠ 0) x Hx).
We prove the intermediate claim Hcl_sub: closure_of X Tx nz_h ⊆ closure_of X Tx nz_f.
An exact proof term for the current goal is (closure_monotone X Tx nz_h nz_f HTx Hnz_h_sub Hnz_f_subX).
Let x be given.
Assume Hx: x ∈ support_of X Tx h.
We will prove x ∈ support_of X Tx f.
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_f: support_of X Tx f = closure_of X Tx nz_f.
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_f.
An exact proof term for the current goal is (Hcl_sub x Hxclh).
rewrite the current goal using Hdef_f (from left to right).
An exact proof term for the current goal is Hxcl.
∎