let A, B be strict MetrStruct ; :: thesis: ( 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))) ) ; :: thesis: 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)

( 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))) ) ; :: thesis: 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

hence
A = B
by A4, A6, BINOP_1:1; :: thesis: verum
let a, b be set ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum

end;assume A8: ( a in the carrier of A & b in the carrier of A ) ; :: thesis: 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; :: thesis: verum