Let I and Xi be given.

Assume HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).

Set X to be the term product_space I Xi.

Set B to be the term box_basis I Xi.

We prove the intermediate claim HBasis: basis_on X B.

An exact proof term for the current goal is (box_basis_is_basis_on I Xi HcompTop).

An exact proof term for the current goal is (lemma_topology_from_basis X B HBasis).

∎