let A, B be strict MetrStruct ; ( the carrier of A = [: the carrier of M, the carrier of N:] & ( for x, y being Point of A ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of A . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) & 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))) ) ) implies A = B )
assume that
A4:
the carrier of A = [: the carrier of M, the carrier of N:]
and
A5:
for x, y being Point of A ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of A . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )
and
A6:
the carrier of B = [: the carrier of M, the carrier of N:]
and
A7:
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))) )
; A = B
set f = the distance of A;
set g = the distance of B;
for a, b being set st a in the carrier of A & b in the carrier of A holds
the distance of A . (a,b) = the distance of B . (a,b)
proof
let a,
b be
set ;
( a in the carrier of A & b in the carrier of A implies the distance of A . (a,b) = the distance of B . (a,b) )
assume A8:
(
a in the
carrier of
A &
b in the
carrier of
A )
;
the distance of A . (a,b) = the distance of B . (a,b)
then consider x1,
y1 being
Point of
M,
x2,
y2 being
Point of
N such that A9:
a = [x1,x2]
and A10:
b = [y1,y2]
and A11:
the
distance of
A . (
a,
b)
= max (
( the distance of M . (x1,y1)),
( the distance of N . (x2,y2)))
by A5;
consider m1,
n1 being
Point of
M,
m2,
n2 being
Point of
N such that A12:
a = [m1,m2]
and A13:
b = [n1,n2]
and A14:
the
distance of
B . (
a,
b)
= max (
( the distance of M . (m1,n1)),
( the distance of N . (m2,n2)))
by A4, A6, A7, A8;
A15:
y1 = n1
by A10, A13, XTUPLE_0:1;
(
x1 = m1 &
x2 = m2 )
by A9, A12, XTUPLE_0:1;
hence
the
distance of
A . (
a,
b)
= the
distance of
B . (
a,
b)
by A10, A11, A13, A14, A15, XTUPLE_0:1;
verum
end;
hence
A = B
by A4, A6, BINOP_1:1; verum