:: Metrics in Cartesian Product
:: by Stanis{\l}awa Kanas and Jan Stankiewicz
::
:: Received September 27, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

scheme :: METRIC_3:sch 1
LambdaMCART{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4( set , set , set , set ) ->  Element of F3() } :
 ex f being Function of [:[:F1(),F2():],[:F1(),F2():]:],F3() st
for x1, y1 being Element of F1()
for x2, y2 being Element of F2()
for x, y being Element of [:F1(),F2():] st x = [x1,x2] & y = [y1,y2] holds
f . (x,y) = F4(x1,y1,x2,y2)
proofend;

definition
let X, Y be non empty MetrSpace;
func dist_cart2 (X,Y) ->  Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL means :Def1: :: METRIC_3:def 1
 for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
it . (x,y) = (dist (x1,y1)) + (dist (x2,y2));
existence
 ex b1 being Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL st
for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
b1 . (x,y) = (dist (x1,y1)) + (dist (x2,y2))
proofend;
uniqueness
 for b1, b2 being Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL st ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
b1 . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) ) & ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
b2 . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines dist_cart2 METRIC_3:def_1_:_
 for X, Y being non empty MetrSpace
for b3 being Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL holds
( b3 = dist_cart2 (X,Y) iff for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
b3 . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) );

theorem Th1: :: METRIC_3:1
for X, Y being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y:] holds
( (dist_cart2 (X,Y)) . (x,y) = 0 iff x = y )
proofend;

theorem Th2: :: METRIC_3:2
for X, Y being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y:] holds (dist_cart2 (X,Y)) . (x,y) = (dist_cart2 (X,Y)) . (y,x)
proofend;

theorem Th3: :: METRIC_3:3
for X, Y being non empty MetrSpace
for x, y, z being Element of [: the carrier of X, the carrier of Y:] holds (dist_cart2 (X,Y)) . (x,z) <= ((dist_cart2 (X,Y)) . (x,y)) + ((dist_cart2 (X,Y)) . (y,z))
proofend;

definition
let X, Y be non empty MetrSpace;
let x, y be Element of [: the carrier of X, the carrier of Y:];
func dist2 (x,y) ->  Real equals :: METRIC_3:def 2
(dist_cart2 (X,Y)) . (x,y);
coherence
 (dist_cart2 (X,Y)) . (x,y) is Real ;
end;

:: deftheorem  defines dist2 METRIC_3:def_2_:_
 for X, Y being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y:] holds dist2 (x,y) = (dist_cart2 (X,Y)) . (x,y);

registration
let A be non empty set ;
let r be Function of [:A,A:],REAL;
cluster MetrStruct(# A,r #) ->  non empty ;
coherence
 not MetrStruct(# A,r #) is empty ;
end;

definition
let X, Y be non empty MetrSpace;
func MetrSpaceCart2 (X,Y) ->  non empty strict MetrSpace equals :: METRIC_3:def 3
 MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2 (X,Y)) #);
coherence
 MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2 (X,Y)) #) is non empty strict MetrSpace
proofend;
end;

:: deftheorem  defines MetrSpaceCart2 METRIC_3:def_3_:_
 for X, Y being non empty MetrSpace holds MetrSpaceCart2 (X,Y) = MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2 (X,Y)) #);

scheme :: METRIC_3:sch 2
LambdaMCART1{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4() ->  non empty set , F5( set , set , set , set , set , set ) ->  Element of F4() } :
 ex f being Function of [:[:F1(),F2(),F3():],[:F1(),F2(),F3():]:],F4() st
for x1, y1 being Element of F1()
for x2, y2 being Element of F2()
for x3, y3 being Element of F3()
for x, y being Element of [:F1(),F2(),F3():] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
f . (x,y) = F5(x1,y1,x2,y2,x3,y3)
proofend;

definition
let X, Y, Z be non empty MetrSpace;
func dist_cart3 (X,Y,Z) ->  Function of [:[: the carrier of X, the carrier of Y, the carrier of Z:],[: the carrier of X, the carrier of Y, the carrier of Z:]:],REAL means :Def4: :: METRIC_3:def 4
 for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
it . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3));
existence
 ex b1 being Function of [:[: the carrier of X, the carrier of Y, the carrier of Z:],[: the carrier of X, the carrier of Y, the carrier of Z:]:],REAL st
for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3))
proofend;
uniqueness
 for b1, b2 being Function of [:[: the carrier of X, the carrier of Y, the carrier of Z:],[: the carrier of X, the carrier of Y, the carrier of Z:]:],REAL st ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) ) &amp; ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines dist_cart3 METRIC_3:def_4_:_
 for X, Y, Z being non empty MetrSpace
for b4 being Function of [:[: the carrier of X, the carrier of Y, the carrier of Z:],[: the carrier of X, the carrier of Y, the carrier of Z:]:],REAL holds
( b4 = dist_cart3 (X,Y,Z) iff for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b4 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) );

theorem Th4: :: METRIC_3:4
for X, Y, Z being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds
( (dist_cart3 (X,Y,Z)) . (x,y) = 0 iff x = y )
proofend;

theorem Th5: :: METRIC_3:5
for X, Y, Z being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds (dist_cart3 (X,Y,Z)) . (x,y) = (dist_cart3 (X,Y,Z)) . (y,x)
proofend;

theorem Th6: :: METRIC_3:6
for X, Y, Z being non empty MetrSpace
for x, y, z being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds (dist_cart3 (X,Y,Z)) . (x,z) <= ((dist_cart3 (X,Y,Z)) . (x,y)) + ((dist_cart3 (X,Y,Z)) . (y,z))
proofend;

definition
let X, Y, Z be non empty MetrSpace;
func MetrSpaceCart3 (X,Y,Z) ->  non empty strict MetrSpace equals :: METRIC_3:def 5
 MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3 (X,Y,Z)) #);
coherence
 MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3 (X,Y,Z)) #) is non empty strict MetrSpace
proofend;
end;

:: deftheorem  defines MetrSpaceCart3 METRIC_3:def_5_:_
 for X, Y, Z being non empty MetrSpace holds MetrSpaceCart3 (X,Y,Z) = MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3 (X,Y,Z)) #);

definition
let X, Y, Z be non empty MetrSpace;
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:];
func dist3 (x,y) ->  Real equals :: METRIC_3:def 6
(dist_cart3 (X,Y,Z)) . (x,y);
coherence
 (dist_cart3 (X,Y,Z)) . (x,y) is Real ;
end;

:: deftheorem  defines dist3 METRIC_3:def_6_:_
 for X, Y, Z being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds dist3 (x,y) = (dist_cart3 (X,Y,Z)) . (x,y);

scheme :: METRIC_3:sch 3
LambdaMCART2{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4() ->  non empty set , F5() ->  non empty set , F6( set , set , set , set , set , set , set , set ) ->  Element of F5() } :
 ex f being Function of [:[:F1(),F2(),F3(),F4():],[:F1(),F2(),F3(),F4():]:],F5() st
for x1, y1 being Element of F1()
for x2, y2 being Element of F2()
for x3, y3 being Element of F3()
for x4, y4 being Element of F4()
for x, y being Element of [:F1(),F2(),F3(),F4():] st x = [x1,x2,x3,x4] &amp; y = [y1,y2,y3,y4] holds
f . (x,y) = F6(x1,y1,x2,y2,x3,y3,x4,y4)
proofend;

definition
let X, Y, Z, W be non empty MetrSpace;
func dist_cart4 (X,Y,Z,W) ->  Function of [:[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]:],REAL means :Def7: :: METRIC_3:def 7
 for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x4, y4 being Element of W
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] &amp; y = [y1,y2,y3,y4] holds
it . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4)));
existence
 ex b1 being Function of [:[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]:],REAL st
for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x4, y4 being Element of W
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] &amp; y = [y1,y2,y3,y4] holds
b1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4)))
proofend;
uniqueness
 for b1, b2 being Function of [:[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]:],REAL st ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x4, y4 being Element of W
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] &amp; y = [y1,y2,y3,y4] holds
b1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ) &amp; ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x4, y4 being Element of W
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] &amp; y = [y1,y2,y3,y4] holds
b2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines dist_cart4 METRIC_3:def_7_:_
 for X, Y, Z, W being non empty MetrSpace
for b5 being Function of [:[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]:],REAL holds
( b5 = dist_cart4 (X,Y,Z,W) iff for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x4, y4 being Element of W
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] &amp; y = [y1,y2,y3,y4] holds
b5 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) );

theorem Th7: :: METRIC_3:7
for X, Y, Z, W being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] holds
( (dist_cart4 (X,Y,Z,W)) . (x,y) = 0 iff x = y )
proofend;

theorem Th8: :: METRIC_3:8
for X, Y, Z, W being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] holds (dist_cart4 (X,Y,Z,W)) . (x,y) = (dist_cart4 (X,Y,Z,W)) . (y,x)
proofend;

theorem Th9: :: METRIC_3:9
for X, Y, Z, W being non empty MetrSpace
for x, y, z being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] holds (dist_cart4 (X,Y,Z,W)) . (x,z) <= ((dist_cart4 (X,Y,Z,W)) . (x,y)) + ((dist_cart4 (X,Y,Z,W)) . (y,z))
proofend;

definition
let X, Y, Z, W be non empty MetrSpace;
func MetrSpaceCart4 (X,Y,Z,W) ->  non empty strict MetrSpace equals :: METRIC_3:def 8
 MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],(dist_cart4 (X,Y,Z,W)) #);
coherence
 MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],(dist_cart4 (X,Y,Z,W)) #) is non empty strict MetrSpace
proofend;
end;

:: deftheorem  defines MetrSpaceCart4 METRIC_3:def_8_:_
 for X, Y, Z, W being non empty MetrSpace holds MetrSpaceCart4 (X,Y,Z,W) = MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],(dist_cart4 (X,Y,Z,W)) #);

definition
let X, Y, Z, W be non empty MetrSpace;
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:];
func dist4 (x,y) ->  Real equals :: METRIC_3:def 9
(dist_cart4 (X,Y,Z,W)) . (x,y);
coherence
 (dist_cart4 (X,Y,Z,W)) . (x,y) is Real ;
end;

:: deftheorem  defines dist4 METRIC_3:def_9_:_
 for X, Y, Z, W being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] holds dist4 (x,y) = (dist_cart4 (X,Y,Z,W)) . (x,y);

begin

definition
let X, Y be non empty MetrSpace;
func dist_cart2S (X,Y) ->  Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL means :Def10: :: METRIC_3:def 10
 for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] &amp; y = [y1,y2] holds
it . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2));
existence
 ex b1 being Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL st
for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] &amp; y = [y1,y2] holds
b1 . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2))
proofend;
uniqueness
 for b1, b2 being Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL st ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] &amp; y = [y1,y2] holds
b1 . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) ) &amp; ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] &amp; y = [y1,y2] holds
b2 . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines dist_cart2S METRIC_3:def_10_:_
 for X, Y being non empty MetrSpace
for b3 being Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL holds
( b3 = dist_cart2S (X,Y) iff for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] &amp; y = [y1,y2] holds
b3 . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) );

Lm1:  for a, b being real number st 0 <= a &amp; 0 <= b holds
( sqrt (a + b) = 0 iff ( a = 0 &amp; b = 0 ) )
by SQUARE_1:31;

theorem Th10: :: METRIC_3:10
for X, Y being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y:] holds
( (dist_cart2S (X,Y)) . (x,y) = 0 iff x = y )
proofend;

theorem Th11: :: METRIC_3:11
for X, Y being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y:] holds (dist_cart2S (X,Y)) . (x,y) = (dist_cart2S (X,Y)) . (y,x)
proofend;

theorem Th12: :: METRIC_3:12
for a, b, c, d being real number st 0 <= a &amp; 0 <= b &amp; 0 <= c &amp; 0 <= d holds
sqrt (((a + c) ^2) + ((b + d) ^2)) <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2)))
proofend;

theorem Th13: :: METRIC_3:13
for X, Y being non empty MetrSpace
for x, y, z being Element of [: the carrier of X, the carrier of Y:] holds (dist_cart2S (X,Y)) . (x,z) <= ((dist_cart2S (X,Y)) . (x,y)) + ((dist_cart2S (X,Y)) . (y,z))
proofend;

definition
let X, Y be non empty MetrSpace;
let x, y be Element of [: the carrier of X, the carrier of Y:];
func dist2S (x,y) ->  Real equals :: METRIC_3:def 11
(dist_cart2S (X,Y)) . (x,y);
coherence
 (dist_cart2S (X,Y)) . (x,y) is Real ;
end;

:: deftheorem  defines dist2S METRIC_3:def_11_:_
 for X, Y being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y:] holds dist2S (x,y) = (dist_cart2S (X,Y)) . (x,y);

definition
let X, Y be non empty MetrSpace;
func MetrSpaceCart2S (X,Y) ->  non empty strict MetrSpace equals :: METRIC_3:def 12
 MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #);
coherence
 MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #) is non empty strict MetrSpace
proofend;
end;

:: deftheorem  defines MetrSpaceCart2S METRIC_3:def_12_:_
 for X, Y being non empty MetrSpace holds MetrSpaceCart2S (X,Y) = MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #);

begin

definition
let X, Y, Z be non empty MetrSpace;
func dist_cart3S (X,Y,Z) ->  Function of [:[: the carrier of X, the carrier of Y, the carrier of Z:],[: the carrier of X, the carrier of Y, the carrier of Z:]:],REAL means :Def13: :: METRIC_3:def 13
 for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
it . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2));
existence
 ex b1 being Function of [:[: the carrier of X, the carrier of Y, the carrier of Z:],[: the carrier of X, the carrier of Y, the carrier of Z:]:],REAL st
for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b1 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))
proofend;
uniqueness
 for b1, b2 being Function of [:[: the carrier of X, the carrier of Y, the carrier of Z:],[: the carrier of X, the carrier of Y, the carrier of Z:]:],REAL st ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b1 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) ) &amp; ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b2 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines dist_cart3S METRIC_3:def_13_:_
 for X, Y, Z being non empty MetrSpace
for b4 being Function of [:[: the carrier of X, the carrier of Y, the carrier of Z:],[: the carrier of X, the carrier of Y, the carrier of Z:]:],REAL holds
( b4 = dist_cart3S (X,Y,Z) iff for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b4 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) );

theorem Th14: :: METRIC_3:14
for X, Y, Z being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds
( (dist_cart3S (X,Y,Z)) . (x,y) = 0 iff x = y )
proofend;

theorem Th15: :: METRIC_3:15
for X, Y, Z being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds (dist_cart3S (X,Y,Z)) . (x,y) = (dist_cart3S (X,Y,Z)) . (y,x)
proofend;

theorem Th16: :: METRIC_3:16
for a, b, c, d, e, f being real number holds (((2 * (a * d)) * (c * b)) + ((2 * (a * f)) * (e * c))) + ((2 * (b * f)) * (e * d)) <= ((((((a * d) ^2) + ((c * b) ^2)) + ((a * f) ^2)) + ((e * c) ^2)) + ((b * f) ^2)) + ((e * d) ^2)
proofend;

theorem Th17: :: METRIC_3:17
for a, b, c, d, e, f being real number holds (((a * c) + (b * d)) + (e * f)) ^2 <= (((a ^2) + (b ^2)) + (e ^2)) * (((c ^2) + (d ^2)) + (f ^2))
proofend;

Lm2:  for a, b, c, d, e, f being real number st 0 <= a &amp; 0 <= b &amp; 0 <= c &amp; 0 <= d &amp; 0 <= e &amp; 0 <= f holds
sqrt ((((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2)) <= (sqrt (((a ^2) + (b ^2)) + (e ^2))) + (sqrt (((c ^2) + (d ^2)) + (f ^2)))
proofend;

theorem Th18: :: METRIC_3:18
for X, Y, Z being non empty MetrSpace
for x, y, z being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds (dist_cart3S (X,Y,Z)) . (x,z) <= ((dist_cart3S (X,Y,Z)) . (x,y)) + ((dist_cart3S (X,Y,Z)) . (y,z))
proofend;

definition
let X, Y, Z be non empty MetrSpace;
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:];
func dist3S (x,y) ->  Real equals :: METRIC_3:def 14
(dist_cart3S (X,Y,Z)) . (x,y);
coherence
 (dist_cart3S (X,Y,Z)) . (x,y) is Real ;
end;

:: deftheorem  defines dist3S METRIC_3:def_14_:_
 for X, Y, Z being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds dist3S (x,y) = (dist_cart3S (X,Y,Z)) . (x,y);

definition
let X, Y, Z be non empty MetrSpace;
func MetrSpaceCart3S (X,Y,Z) ->  non empty strict MetrSpace equals :: METRIC_3:def 15
 MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3S (X,Y,Z)) #);
coherence
 MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3S (X,Y,Z)) #) is non empty strict MetrSpace
proofend;
end;

:: deftheorem  defines MetrSpaceCart3S METRIC_3:def_15_:_
 for X, Y, Z being non empty MetrSpace holds MetrSpaceCart3S (X,Y,Z) = MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3S (X,Y,Z)) #);

definition
func taxi_dist2  ->  Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means :Def16: :: METRIC_3:def 16
 for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] &amp; y = [y1,y2] holds
it . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2));
existence
 ex b1 being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL st
for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] &amp; y = [y1,y2] holds
b1 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2))
proofend;
uniqueness
 for b1, b2 being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL st ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] &amp; y = [y1,y2] holds
b1 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) ) &amp; ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] &amp; y = [y1,y2] holds
b2 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines taxi_dist2 METRIC_3:def_16_:_
 for b1 being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL holds
( b1 = taxi_dist2 iff for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] &amp; y = [y1,y2] holds
b1 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) );

theorem Th19: :: METRIC_3:19
for x, y being Element of [:REAL,REAL:] holds
( taxi_dist2 . (x,y) = 0 iff x = y )
proofend;

theorem Th20: :: METRIC_3:20
for x, y being Element of [:REAL,REAL:] holds taxi_dist2 . (x,y) = taxi_dist2 . (y,x)
proofend;

theorem Th21: :: METRIC_3:21
for x, y, z being Element of [:REAL,REAL:] holds taxi_dist2 . (x,z) <= (taxi_dist2 . (x,y)) + (taxi_dist2 . (y,z))
proofend;

definition
func RealSpaceCart2  ->  non empty strict MetrSpace equals :: METRIC_3:def 17
 MetrStruct(# [:REAL,REAL:],taxi_dist2 #);
coherence
 MetrStruct(# [:REAL,REAL:],taxi_dist2 #) is non empty strict MetrSpace
proofend;
end;

:: deftheorem  defines RealSpaceCart2 METRIC_3:def_17_:_
 RealSpaceCart2 = MetrStruct(# [:REAL,REAL:],taxi_dist2 #);

definition
func Eukl_dist2  ->  Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means :Def18: :: METRIC_3:def 18
 for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] &amp; y = [y1,y2] holds
it . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2));
existence
 ex b1 being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL st
for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] &amp; y = [y1,y2] holds
b1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))
proofend;
uniqueness
 for b1, b2 being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL st ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] &amp; y = [y1,y2] holds
b1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ) &amp; ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] &amp; y = [y1,y2] holds
b2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def18 defines Eukl_dist2 METRIC_3:def_18_:_
 for b1 being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL holds
( b1 = Eukl_dist2 iff for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] &amp; y = [y1,y2] holds
b1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) );

theorem Th22: :: METRIC_3:22
for x, y being Element of [:REAL,REAL:] holds
( Eukl_dist2 . (x,y) = 0 iff x = y )
proofend;

theorem Th23: :: METRIC_3:23
for x, y being Element of [:REAL,REAL:] holds Eukl_dist2 . (x,y) = Eukl_dist2 . (y,x)
proofend;

theorem Th24: :: METRIC_3:24
for x, y, z being Element of [:REAL,REAL:] holds Eukl_dist2 . (x,z) <= (Eukl_dist2 . (x,y)) + (Eukl_dist2 . (y,z))
proofend;

definition
func EuklSpace2  ->  non empty strict MetrSpace equals :: METRIC_3:def 19
 MetrStruct(# [:REAL,REAL:],Eukl_dist2 #);
coherence
 MetrStruct(# [:REAL,REAL:],Eukl_dist2 #) is non empty strict MetrSpace
proofend;
end;

:: deftheorem  defines EuklSpace2 METRIC_3:def_19_:_
 EuklSpace2 = MetrStruct(# [:REAL,REAL:],Eukl_dist2 #);

definition
func taxi_dist3  ->  Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL means :Def20: :: METRIC_3:def 20
 for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
it . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3));
existence
 ex b1 being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL st
for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b1 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3))
proofend;
uniqueness
 for b1, b2 being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL st ( for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b1 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) ) &amp; ( for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b2 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def20 defines taxi_dist3 METRIC_3:def_20_:_
 for b1 being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL holds
( b1 = taxi_dist3 iff for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b1 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) );

theorem Th25: :: METRIC_3:25
for x, y being Element of [:REAL,REAL,REAL:] holds
( taxi_dist3 . (x,y) = 0 iff x = y )
proofend;

theorem Th26: :: METRIC_3:26
for x, y being Element of [:REAL,REAL,REAL:] holds taxi_dist3 . (x,y) = taxi_dist3 . (y,x)
proofend;

theorem Th27: :: METRIC_3:27
for x, y, z being Element of [:REAL,REAL,REAL:] holds taxi_dist3 . (x,z) <= (taxi_dist3 . (x,y)) + (taxi_dist3 . (y,z))
proofend;

definition
func RealSpaceCart3  ->  non empty strict MetrSpace equals :: METRIC_3:def 21
 MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #);
coherence
 MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #) is non empty strict MetrSpace
proofend;
end;

:: deftheorem  defines RealSpaceCart3 METRIC_3:def_21_:_
 RealSpaceCart3 = MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #);

definition
func Eukl_dist3  ->  Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL means :Def22: :: METRIC_3:def 22
 for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
it . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2));
existence
 ex b1 being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL st
for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b1 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))
proofend;
uniqueness
 for b1, b2 being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL st ( for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b1 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) ) &amp; ( for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b2 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def22 defines Eukl_dist3 METRIC_3:def_22_:_
 for b1 being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL holds
( b1 = Eukl_dist3 iff for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] &amp; y = [y1,y2,y3] holds
b1 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) );

theorem Th28: :: METRIC_3:28
for x, y being Element of [:REAL,REAL,REAL:] holds
( Eukl_dist3 . (x,y) = 0 iff x = y )
proofend;

theorem Th29: :: METRIC_3:29
for x, y being Element of [:REAL,REAL,REAL:] holds Eukl_dist3 . (x,y) = Eukl_dist3 . (y,x)
proofend;

theorem Th30: :: METRIC_3:30
for x, y, z being Element of [:REAL,REAL,REAL:] holds Eukl_dist3 . (x,z) <= (Eukl_dist3 . (x,y)) + (Eukl_dist3 . (y,z))
proofend;

definition
func EuklSpace3  ->  non empty strict MetrSpace equals :: METRIC_3:def 23
 MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #);
coherence
 MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #) is non empty strict MetrSpace
proofend;
end;

:: deftheorem  defines EuklSpace3 METRIC_3:def_23_:_
 EuklSpace3 = MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #);