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

proof

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] & b = [y1,y2] ) and
A10: 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
A11: ( a = [m1,m2] & b = [n1,n2] ) and
A12: the distance of B . a,b = max (the distance of M . m1,n1),(the distance of N . m2,n2) by A4, A6, A7, A8;
( x1 = m1 & x2 = m2 & y1 = n1 & y2 = n2 ) by A9, A11, ZFMISC_1:33;
hence the distance of A . a,b = the distance of B . a,b by A10, A12; :: thesis: verum

end;

hence A = B by A4, A6, BINOP_1:1; :: thesis: verum