:: deftheorem Def1 defines max-Prod2 TOPREAL7:def 1 :
for M, N being non empty MetrStruct
for b₃ being strict MetrStruct holds
( b₃ = max-Prod2 (M,N) iff ( the carrier of b₃ = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b₃ ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b₃ . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) ) );