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, ZFMISC_1:33;
(
x1 = m1 &
x2 = m2 )
by A9, A12, ZFMISC_1:33;
hence
the
distance of
A . a,
b = the
distance of
B . a,
b
by A10, A11, A13, A14, A15, ZFMISC_1:33;
verum
end;
hence
A = B
by A4, A6, BINOP_1:1; verum