Let X, Tx, g and c be given.

Assume HTx: topology_on X Tx.

Assume Hg: continuous_map X Tx R R_standard_topology g.

Assume HcR: c ∈ R.

Assume Hcpos: 0 < c.

We will prove continuous_map X Tx R R_standard_topology (compose_fun X g (mul_const_fun c)).

We prove the intermediate claim Hmulcont: continuous_map R R_standard_topology R R_standard_topology (mul_const_fun c).

An exact proof term for the current goal is (mul_const_fun_continuous_pos c HcR Hcpos).

An exact proof term for the current goal is (composition_continuous X Tx R R_standard_topology R R_standard_topology g (mul_const_fun c) Hg Hmulcont).

∎