theorem :: EUCLID_9:28

for n being Nat holds TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1)