for M, N being non empty MetrSpace holds [:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N))