This article covers some technical aspects about the product topology which are usually not given much of a thought in mathematics and standard literature like [7] and [6], not even by Bourbaki in [4].
Let {Ti}i∈I be a family of topological spaces. The prebasis of the product space T = ∏i∈I Ti is defined in [5] as the set of all π−1i(V) with i ∈ I and V open in Ti. Here it is shown that the basis generated by this prebasis consists exactly of the sets ∏i∈I Vi with Vi open in Ti and for all but finitely many i ∈ I holds Vi = Ti. Given I = {a} we have T ≅ Ta, given I = {a, b} with a≠ b we have T ≅ Ta ×Tb. Given another family of topological spaces {Si}i∈I such that Si ≅ Ti for all i ∈ I, we have S = ∏i∈I Si ≅ T. If instead Si is a subspace of Ti for each i ∈ I, then S is a subspace of T.
These results are obvious for mathematicians, but formally proven here by means of the Mizar system [3], [2].