theorem :: TOPREAL7:25

for i, j being Element of NAT holds [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], TopSpaceMetr (Euclid (i + j)) are_homeomorphic