let M, N be non empty MetrStruct ; for m1, m2 being Point of M
for n1, n2 being Point of N holds dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2)))
let m1, m2 be Point of M; for n1, n2 being Point of N holds dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2)))
let n1, n2 be Point of N; dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2)))
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1:
[m1,n1] = [x1,x2]
and
A2:
[m2,n2] = [y1,y2]
and
A3:
the distance of (max-Prod2 (M,N)) . ([m1,n1],[m2,n2]) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2)))
by Def1;
A4:
m2 = y1
by A2, XTUPLE_0:1;
( m1 = x1 & n1 = x2 )
by A1, XTUPLE_0:1;
hence
dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2)))
by A2, A3, A4, XTUPLE_0:1; verum