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