:: METRIC_3 semantic presentation

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)
proof
deffunc H1( Element of [:F1(),F2():], Element of [:F1(),F2():]) ->  Element of F3() = F4(($1 `1),($2 `1),($1 `2),($2 `2));
consider f being Function of [:[:F1(),F2():],[:F1(),F2():]:],F3() such that
A1: for x, y being Element of [:F1(),F2():] holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  f ; ::_thesis: 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)
let x1, y1 be Element of F1(); ::_thesis: 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)
let x2, y2 be Element of F2(); ::_thesis: for x, y being Element of [:F1(),F2():] st x = [x1,x2] & y = [y1,y2] holds
f . (x,y) = F4(x1,y1,x2,y2)
let x, y be Element of [:F1(),F2():]; ::_thesis: ( x = [x1,x2] & y = [y1,y2] implies f . (x,y) = F4(x1,y1,x2,y2) )
assume that
A2: x = [x1,x2] and
A3: y = [y1,y2] ; ::_thesis: f . (x,y) = F4(x1,y1,x2,y2)
 y = [(y `1),(y `2)] by MCART_1:21;
then A4: ( y1 = y `1 & y2 = y `2 ) by A3, XTUPLE_0:1;
 x = [(x `1),(x `2)] by MCART_1:21;
then  ( x1 = x `1 & x2 = x `2 ) by A2, XTUPLE_0:1;
hence  f . (x,y) = F4(x1,y1,x2,y2) by A1, A4; ::_thesis: verum
end;

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))
proof
deffunc H1( Element of X, Element of X, Element of Y, Element of Y) ->  Element of REAL = (dist ($1,$2)) + (dist ($3,$4));
consider F being Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL such that
A1: 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
F . (x,y) = H1(x1,y1,x2,y2) from METRIC_3:sch_1();
take  F ; ::_thesis: 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
F . (x,y) = (dist (x1,y1)) + (dist (x2,y2))
let x1, y1 be Element of X; ::_thesis: 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
F . (x,y) = (dist (x1,y1)) + (dist (x2,y2))
let x2, y2 be Element of Y; ::_thesis: for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
F . (x,y) = (dist (x1,y1)) + (dist (x2,y2))
let x, y be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: ( x = [x1,x2] & y = [y1,y2] implies F . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) )
assume  ( x = [x1,x2] & y = [y1,y2] ) ; ::_thesis: F . (x,y) = (dist (x1,y1)) + (dist (x2,y2))
hence  F . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) by A1; ::_thesis: verum
end;
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
proof
let f1, f2 be Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL; ::_thesis: ( ( 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
f1 . (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
f2 . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) ) implies f1 = f2 )
assume that
A2: 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
f1 . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) and
A3: 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
f2 . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) ; ::_thesis: f1 = f2
 for x, y being Element of [: the carrier of X, the carrier of Y:] holds f1 . (x,y) = f2 . (x,y)
proof
let x, y be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: f1 . (x,y) = f2 . (x,y)
consider x1 being Element of X, x2 being Element of Y such that
A4: x = [x1,x2] by DOMAIN_1:1;
consider y1 being Element of X, y2 being Element of Y such that
A5: y = [y1,y2] by DOMAIN_1:1;
thus f1 . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) by A2, A4, A5
.= f2 . (x,y) by A3, A4, A5 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
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 )
proof
let X, Y be non empty MetrSpace; ::_thesis: 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 )
let x, y be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: ( (dist_cart2 (X,Y)) . (x,y) = 0 iff x = y )
reconsider x1 = x `1 , y1 = y `1 as Element of X ;
reconsider x2 = x `2 , y2 = y `2 as Element of Y ;
A1: ( x = [x1,x2] & y = [y1,y2] ) by MCART_1:22;
thus  ( (dist_cart2 (X,Y)) . (x,y) = 0 implies x = y ) ::_thesis: ( x = y implies (dist_cart2 (X,Y)) . (x,y) = 0 )
proof
set d1 = dist (x1,y1);
set d2 = dist (x2,y2);
assume  (dist_cart2 (X,Y)) . (x,y) = 0 ; ::_thesis: x = y
then A2: (dist (x1,y1)) + (dist (x2,y2)) = 0 by A1, Def1;
A3: ( 0 <= dist (x1,y1) & 0 <= dist (x2,y2) ) by METRIC_1:5;
then  dist (x1,y1) = 0 by A2, XREAL_1:27;
then A4: x1 = y1 by METRIC_1:2;
 dist (x2,y2) = 0 by A2, A3, XREAL_1:27;
hence  x = y by A1, A4, METRIC_1:2; ::_thesis: verum
end;
assume A5: x = y ; ::_thesis: (dist_cart2 (X,Y)) . (x,y) = 0
then A6: dist (x2,y2) = 0 by METRIC_1:1;
(dist_cart2 (X,Y)) . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) by A1, Def1
.= 0 by A5, A6, METRIC_1:1 ;
hence  (dist_cart2 (X,Y)) . (x,y) = 0 ; ::_thesis: verum
end;

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)
proof
let X, Y be non empty MetrSpace; ::_thesis: 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)
let x, y be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: (dist_cart2 (X,Y)) . (x,y) = (dist_cart2 (X,Y)) . (y,x)
reconsider x1 = x `1 , y1 = y `1 as Element of X ;
reconsider x2 = x `2 , y2 = y `2 as Element of Y ;
A1: ( x = [x1,x2] & y = [y1,y2] ) by MCART_1:22;
then (dist_cart2 (X,Y)) . (x,y) = (dist (y1,x1)) + (dist (x2,y2)) by Def1
.= (dist_cart2 (X,Y)) . (y,x) by A1, Def1 ;
hence  (dist_cart2 (X,Y)) . (x,y) = (dist_cart2 (X,Y)) . (y,x) ; ::_thesis: verum
end;

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))
proof
let X, Y be non empty MetrSpace; ::_thesis: 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))
let x, y, z be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: (dist_cart2 (X,Y)) . (x,z) <= ((dist_cart2 (X,Y)) . (x,y)) + ((dist_cart2 (X,Y)) . (y,z))
reconsider x1 = x `1 , y1 = y `1 , z1 = z `1 as Element of X ;
reconsider x2 = x `2 , y2 = y `2 , z2 = z `2 as Element of Y ;
A1: y = [y1,y2] by MCART_1:22;
set d6 = dist (y2,z2);
set d5 = dist (x2,y2);
set d4 = dist (x2,z2);
set d3 = dist (y1,z1);
set d2 = dist (x1,y1);
set d1 = dist (x1,z1);
A2: z = [z1,z2] by MCART_1:22;
A3: x = [x1,x2] by MCART_1:22;
then A4: (dist_cart2 (X,Y)) . (x,z) = (dist (x1,z1)) + (dist (x2,z2)) by A2, Def1;
A5: ( dist (x1,z1) <= (dist (x1,y1)) + (dist (y1,z1)) & dist (x2,z2) <= (dist (x2,y2)) + (dist (y2,z2)) ) by METRIC_1:4;
((dist (x1,y1)) + (dist (y1,z1))) + ((dist (x2,y2)) + (dist (y2,z2))) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (y1,z1)) + (dist (y2,z2)))
.= ((dist_cart2 (X,Y)) . (x,y)) + ((dist (y1,z1)) + (dist (y2,z2))) by A3, A1, Def1
.= ((dist_cart2 (X,Y)) . (x,y)) + ((dist_cart2 (X,Y)) . (y,z)) by A1, A2, Def1 ;
hence  (dist_cart2 (X,Y)) . (x,z) <= ((dist_cart2 (X,Y)) . (x,y)) + ((dist_cart2 (X,Y)) . (y,z)) by A5, A4, XREAL_1:7; ::_thesis: verum
end;

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
proof
set M = MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2 (X,Y)) #);
now__::_thesis:_for_x,_y,_z_being_Element_of_MetrStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],(dist_cart2_(X,Y))_#)_holds_
(_(_dist_(x,y)_=_0_implies_x_=_y_)_&_(_x_=_y_implies_dist_(x,y)_=_0_)_&_dist_(x,y)_=_dist_(y,x)_&_dist_(x,z)_<=_(dist_(x,y))_+_(dist_(y,z))_)
let x, y, z be Element of MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2 (X,Y)) #); ::_thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
A1: dist (x,y) = (dist_cart2 (X,Y)) . (x,y) by METRIC_1:def_1;
hence  ( dist (x,y) = 0 iff x = y ) by Th1; ::_thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
 dist (y,x) = (dist_cart2 (X,Y)) . (y,x) by METRIC_1:def_1;
hence  dist (x,y) = dist (y,x) by A1, Th2; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
 ( dist (x,z) = (dist_cart2 (X,Y)) . (x,z) & dist (y,z) = (dist_cart2 (X,Y)) . (y,z) ) by METRIC_1:def_1;
hence  dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th3; ::_thesis: verum
end;
hence  MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2 (X,Y)) #) is non empty strict MetrSpace by METRIC_1:6; ::_thesis: verum
end;
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] & y = [y1,y2,y3] holds
f . (x,y) = F5(x1,y1,x2,y2,x3,y3)
proof
deffunc H1( Element of [:F1(),F2(),F3():], Element of [:F1(),F2(),F3():]) ->  Element of F4() = F5(($1 `1_3),($2 `1_3),($1 `2_3),($2 `2_3),($1 `3_3),($2 `3_3));
consider f being Function of [:[:F1(),F2(),F3():],[:F1(),F2(),F3():]:],F4() such that
A1: for x, y being Element of [:F1(),F2(),F3():] holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  f ; ::_thesis: 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] & y = [y1,y2,y3] holds
f . (x,y) = F5(x1,y1,x2,y2,x3,y3)
let x1, y1 be Element of F1(); ::_thesis: 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] & y = [y1,y2,y3] holds
f . (x,y) = F5(x1,y1,x2,y2,x3,y3)
let x2, y2 be Element of F2(); ::_thesis: for x3, y3 being Element of F3()
for x, y being Element of [:F1(),F2(),F3():] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
f . (x,y) = F5(x1,y1,x2,y2,x3,y3)
let x3, y3 be Element of F3(); ::_thesis: for x, y being Element of [:F1(),F2(),F3():] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
f . (x,y) = F5(x1,y1,x2,y2,x3,y3)
let x, y be Element of [:F1(),F2(),F3():]; ::_thesis: ( x = [x1,x2,x3] & y = [y1,y2,y3] implies f . (x,y) = F5(x1,y1,x2,y2,x3,y3) )
assume that
A2: x = [x1,x2,x3] and
A3: y = [y1,y2,y3] ; ::_thesis: f . (x,y) = F5(x1,y1,x2,y2,x3,y3)
A4: y = [(y `1_3),(y `2_3),(y `3_3)] by MCART_1:44;
then A5: ( y1 = y `1_3 & y2 = y `2_3 ) by A3, XTUPLE_0:3;
A6: x = [(x `1_3),(x `2_3),(x `3_3)] by MCART_1:44;
then A7: x3 = x `3_3 by A2, XTUPLE_0:3;
A8: y3 = y `3_3 by A3, A4, XTUPLE_0:3;
 ( x1 = x `1_3 & x2 = x `2_3 ) by A2, A6, XTUPLE_0:3;
hence  f . (x,y) = F5(x1,y1,x2,y2,x3,y3) by A1, A5, A7, A8; ::_thesis: verum
end;

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] & 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] & y = [y1,y2,y3] holds
b1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3))
proof
deffunc H1( Element of X, Element of X, Element of Y, Element of Y, Element of Z, Element of Z) ->  Element of REAL = ((dist ($1,$2)) + (dist ($3,$4))) + (dist ($5,$6));
consider F 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 such that
A1: 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] & y = [y1,y2,y3] holds
F . (x,y) = H1(x1,y1,x2,y2,x3,y3) from METRIC_3:sch_2();
take  F ; ::_thesis: 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] & y = [y1,y2,y3] holds
F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3))
let x1, y1 be Element of X; ::_thesis: 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] & y = [y1,y2,y3] holds
F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3))
let x2, y2 be Element of Y; ::_thesis: 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] & y = [y1,y2,y3] holds
F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3))
let x3, y3 be Element of Z; ::_thesis: for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3))
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; ::_thesis: ( x = [x1,x2,x3] & y = [y1,y2,y3] implies F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) )
assume  ( x = [x1,x2,x3] & y = [y1,y2,y3] ) ; ::_thesis: F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3))
hence  F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) by A1; ::_thesis: verum
end;
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] & y = [y1,y2,y3] holds
b1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) ) & ( 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] & y = [y1,y2,y3] holds
b2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) ) holds
b1 = b2
proof
let f1, f2 be 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; ::_thesis: ( ( 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] & y = [y1,y2,y3] holds
f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) ) & ( 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] & y = [y1,y2,y3] holds
f2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) ) implies f1 = f2 )
assume that
A2: 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] & y = [y1,y2,y3] holds
f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) and
A3: 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] & y = [y1,y2,y3] holds
f2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) ; ::_thesis: f1 = f2
 for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds f1 . (x,y) = f2 . (x,y)
proof
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; ::_thesis: f1 . (x,y) = f2 . (x,y)
consider x1 being Element of X, x2 being Element of Y, x3 being Element of Z such that
A4: x = [x1,x2,x3] by DOMAIN_1:3;
consider y1 being Element of X, y2 being Element of Y, y3 being Element of Z such that
A5: y = [y1,y2,y3] by DOMAIN_1:3;
thus f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) by A2, A4, A5
.= f2 . (x,y) by A3, A4, A5 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
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] & 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 )
proof
let X, Y, Z be non empty MetrSpace; ::_thesis: 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 )
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; ::_thesis: ( (dist_cart3 (X,Y,Z)) . (x,y) = 0 iff x = y )
reconsider x1 = x `1_3 , y1 = y `1_3 as Element of X ;
reconsider x2 = x `2_3 , y2 = y `2_3 as Element of Y ;
reconsider x3 = x `3_3 , y3 = y `3_3 as Element of Z ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) by MCART_1:44;
thus  ( (dist_cart3 (X,Y,Z)) . (x,y) = 0 implies x = y ) ::_thesis: ( x = y implies (dist_cart3 (X,Y,Z)) . (x,y) = 0 )
proof
set d3 = dist (x3,y3);
set d2 = dist (x2,y2);
set d1 = dist (x1,y1);
set d4 = (dist (x1,y1)) + (dist (x2,y2));
assume  (dist_cart3 (X,Y,Z)) . (x,y) = 0 ; ::_thesis: x = y
then A2: ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) = 0 by A1, Def4;
A3: ( 0 <= dist (x1,y1) & 0 <= dist (x2,y2) ) by METRIC_1:5;
then A4: ( 0 <= dist (x3,y3) & 0 + 0 <= (dist (x1,y1)) + (dist (x2,y2)) ) by METRIC_1:5, XREAL_1:7;
then A5: (dist (x1,y1)) + (dist (x2,y2)) = 0 by A2, XREAL_1:27;
then  dist (x1,y1) = 0 by A3, XREAL_1:27;
then A6: x1 = y1 by METRIC_1:2;
 dist (x3,y3) = 0 by A2, A4, XREAL_1:27;
then A7: x3 = y3 by METRIC_1:2;
 dist (x2,y2) = 0 by A3, A5, XREAL_1:27;
hence  x = y by A1, A7, A6, METRIC_1:2; ::_thesis: verum
end;
assume A8: x = y ; ::_thesis: (dist_cart3 (X,Y,Z)) . (x,y) = 0
then A9: ( dist (x1,y1) = 0 & dist (x2,y2) = 0 ) by METRIC_1:1;
(dist_cart3 (X,Y,Z)) . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) by A1, Def4
.= 0 by A8, A9, METRIC_1:1 ;
hence  (dist_cart3 (X,Y,Z)) . (x,y) = 0 ; ::_thesis: verum
end;

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)
proof
let X, Y, Z be non empty MetrSpace; ::_thesis: 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)
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; ::_thesis: (dist_cart3 (X,Y,Z)) . (x,y) = (dist_cart3 (X,Y,Z)) . (y,x)
reconsider x1 = x `1_3 , y1 = y `1_3 as Element of X ;
reconsider x2 = x `2_3 , y2 = y `2_3 as Element of Y ;
reconsider x3 = x `3_3 , y3 = y `3_3 as Element of Z ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) by MCART_1:44;
then (dist_cart3 (X,Y,Z)) . (x,y) = ((dist (y1,x1)) + (dist (y2,x2))) + (dist (y3,x3)) by Def4
.= (dist_cart3 (X,Y,Z)) . (y,x) by A1, Def4 ;
hence  (dist_cart3 (X,Y,Z)) . (x,y) = (dist_cart3 (X,Y,Z)) . (y,x) ; ::_thesis: verum
end;

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))
proof
let X, Y, Z be non empty MetrSpace; ::_thesis: 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))
let x, y, z be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; ::_thesis: (dist_cart3 (X,Y,Z)) . (x,z) <= ((dist_cart3 (X,Y,Z)) . (x,y)) + ((dist_cart3 (X,Y,Z)) . (y,z))
reconsider x1 = x `1_3 , y1 = y `1_3 , z1 = z `1_3 as Element of X ;
reconsider x2 = x `2_3 , y2 = y `2_3 , z2 = z `2_3 as Element of Y ;
reconsider x3 = x `3_3 , y3 = y `3_3 , z3 = z `3_3 as Element of Z ;
A1: x = [x1,x2,x3] by MCART_1:44;
set d4 = dist (x2,z2);
set d5 = dist (x2,y2);
set d6 = dist (y2,z2);
A2: z = [z1,z2,z3] by MCART_1:44;
set d7 = dist (x3,z3);
set d8 = dist (x3,y3);
set d9 = dist (y3,z3);
set d1 = dist (x1,z1);
set d2 = dist (x1,y1);
set d3 = dist (y1,z1);
A3: y = [y1,y2,y3] by MCART_1:44;
set d10 = (dist (x1,z1)) + (dist (x2,z2));
 ( dist (x1,z1) <= (dist (x1,y1)) + (dist (y1,z1)) & dist (x2,z2) <= (dist (x2,y2)) + (dist (y2,z2)) ) by METRIC_1:4;
then A4: (dist (x1,z1)) + (dist (x2,z2)) <= ((dist (x1,y1)) + (dist (y1,z1))) + ((dist (x2,y2)) + (dist (y2,z2))) by XREAL_1:7;
 dist (x3,z3) <= (dist (x3,y3)) + (dist (y3,z3)) by METRIC_1:4;
then A5: ((dist (x1,z1)) + (dist (x2,z2))) + (dist (x3,z3)) <= (((dist (x1,y1)) + (dist (y1,z1))) + ((dist (x2,y2)) + (dist (y2,z2)))) + ((dist (x3,y3)) + (dist (y3,z3))) by A4, XREAL_1:7;
(((dist (x1,y1)) + (dist (y1,z1))) + ((dist (x2,y2)) + (dist (y2,z2)))) + ((dist (x3,y3)) + (dist (y3,z3))) = (((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3))) + (((dist (y1,z1)) + (dist (y2,z2))) + (dist (y3,z3)))
.= ((dist_cart3 (X,Y,Z)) . (x,y)) + (((dist (y1,z1)) + (dist (y2,z2))) + (dist (y3,z3))) by A1, A3, Def4
.= ((dist_cart3 (X,Y,Z)) . (x,y)) + ((dist_cart3 (X,Y,Z)) . (y,z)) by A3, A2, Def4 ;
hence  (dist_cart3 (X,Y,Z)) . (x,z) <= ((dist_cart3 (X,Y,Z)) . (x,y)) + ((dist_cart3 (X,Y,Z)) . (y,z)) by A1, A2, A5, Def4; ::_thesis: verum
end;

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
proof
set M = MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3 (X,Y,Z)) #);
now__::_thesis:_for_x,_y,_z_being_Element_of_MetrStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y,_the_carrier_of_Z:],(dist_cart3_(X,Y,Z))_#)_holds_
(_(_dist_(x,y)_=_0_implies_x_=_y_)_&_(_x_=_y_implies_dist_(x,y)_=_0_)_&_dist_(x,y)_=_dist_(y,x)_&_dist_(x,z)_<=_(dist_(x,y))_+_(dist_(y,z))_)
let x, y, z be Element of MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3 (X,Y,Z)) #); ::_thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
A1: dist (x,y) = (dist_cart3 (X,Y,Z)) . (x,y) by METRIC_1:def_1;
hence  ( dist (x,y) = 0 iff x = y ) by Th4; ::_thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
 dist (y,x) = (dist_cart3 (X,Y,Z)) . (y,x) by METRIC_1:def_1;
hence  dist (x,y) = dist (y,x) by A1, Th5; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
 ( dist (x,z) = (dist_cart3 (X,Y,Z)) . (x,z) & dist (y,z) = (dist_cart3 (X,Y,Z)) . (y,z) ) by METRIC_1:def_1;
hence  dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th6; ::_thesis: verum
end;
hence  MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3 (X,Y,Z)) #) is non empty strict MetrSpace by METRIC_1:6; ::_thesis: verum
end;
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] & y = [y1,y2,y3,y4] holds
f . (x,y) = F6(x1,y1,x2,y2,x3,y3,x4,y4)
proof
deffunc H1( Element of [:F1(),F2(),F3(),F4():], Element of [:F1(),F2(),F3(),F4():]) ->  Element of F5() = F6(($1 `1_4),($2 `1_4),($1 `2_4),($2 `2_4),($1 `3_4),($2 `3_4),($1 `4_4),($2 `4_4));
consider f being Function of [:[:F1(),F2(),F3(),F4():],[:F1(),F2(),F3(),F4():]:],F5() such that
A1: for x, y being Element of [:F1(),F2(),F3(),F4():] holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  f ; ::_thesis: 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] & y = [y1,y2,y3,y4] holds
f . (x,y) = F6(x1,y1,x2,y2,x3,y3,x4,y4)
let x1, y1 be Element of F1(); ::_thesis: 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] & y = [y1,y2,y3,y4] holds
f . (x,y) = F6(x1,y1,x2,y2,x3,y3,x4,y4)
let x2, y2 be Element of F2(); ::_thesis: 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] & y = [y1,y2,y3,y4] holds
f . (x,y) = F6(x1,y1,x2,y2,x3,y3,x4,y4)
let x3, y3 be Element of F3(); ::_thesis: for x4, y4 being Element of F4()
for x, y being Element of [:F1(),F2(),F3(),F4():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f . (x,y) = F6(x1,y1,x2,y2,x3,y3,x4,y4)
let x4, y4 be Element of F4(); ::_thesis: for x, y being Element of [:F1(),F2(),F3(),F4():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f . (x,y) = F6(x1,y1,x2,y2,x3,y3,x4,y4)
let x, y be Element of [:F1(),F2(),F3(),F4():]; ::_thesis: ( x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] implies f . (x,y) = F6(x1,y1,x2,y2,x3,y3,x4,y4) )
assume that
A2: x = [x1,x2,x3,x4] and
A3: y = [y1,y2,y3,y4] ; ::_thesis: f . (x,y) = F6(x1,y1,x2,y2,x3,y3,x4,y4)
A4: y = [(y `1_4),(y `2_4),(y `3_4),(y `4_4)] by MCART_1:56;
then A5: ( y1 = y `1_4 & y2 = y `2_4 ) by A3, XTUPLE_0:5;
A6: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] by MCART_1:56;
then A7: ( x3 = x `3_4 & x4 = x `4_4 ) by A2, XTUPLE_0:5;
A8: ( y3 = y `3_4 & y4 = y `4_4 ) by A3, A4, XTUPLE_0:5;
 ( x1 = x `1_4 & x2 = x `2_4 ) by A2, A6, XTUPLE_0:5;
hence  f . (x,y) = F6(x1,y1,x2,y2,x3,y3,x4,y4) by A1, A5, A7, A8; ::_thesis: verum
end;

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] & 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] & y = [y1,y2,y3,y4] holds
b1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4)))
proof
deffunc H1( Element of X, Element of X, Element of Y, Element of Y, Element of Z, Element of Z, Element of W, Element of W) ->  Element of REAL = ((dist ($1,$2)) + (dist ($3,$4))) + ((dist ($5,$6)) + (dist ($7,$8)));
consider F 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 such that
A1: 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] & y = [y1,y2,y3,y4] holds
F . (x,y) = H1(x1,y1,x2,y2,x3,y3,x4,y4) from METRIC_3:sch_3();
take  F ; ::_thesis: 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] & y = [y1,y2,y3,y4] holds
F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4)))
let x1, y1 be Element of X; ::_thesis: 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] & y = [y1,y2,y3,y4] holds
F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4)))
let x2, y2 be Element of Y; ::_thesis: 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] & y = [y1,y2,y3,y4] holds
F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4)))
let x3, y3 be Element of Z; ::_thesis: 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] & y = [y1,y2,y3,y4] holds
F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4)))
let x4, y4 be Element of W; ::_thesis: 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] & y = [y1,y2,y3,y4] holds
F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4)))
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]; ::_thesis: ( x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] implies F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) )
assume  ( x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] ) ; ::_thesis: F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4)))
hence  F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) by A1; ::_thesis: verum
end;
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] & y = [y1,y2,y3,y4] holds
b1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ) & ( 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] & y = [y1,y2,y3,y4] holds
b2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ) holds
b1 = b2
proof
let f1, f2 be 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; ::_thesis: ( ( 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] & y = [y1,y2,y3,y4] holds
f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ) & ( 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] & y = [y1,y2,y3,y4] holds
f2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ) implies f1 = f2 )
assume that
A2: 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] & y = [y1,y2,y3,y4] holds
f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) and
A3: 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] & y = [y1,y2,y3,y4] holds
f2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ; ::_thesis: f1 = f2
 for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] holds f1 . (x,y) = f2 . (x,y)
proof
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]; ::_thesis: f1 . (x,y) = f2 . (x,y)
consider x1 being Element of X, x2 being Element of Y, x3 being Element of Z, x4 being Element of W such that
A4: x = [x1,x2,x3,x4] by DOMAIN_1:10;
consider y1 being Element of X, y2 being Element of Y, y3 being Element of Z, y4 being Element of W such that
A5: y = [y1,y2,y3,y4] by DOMAIN_1:10;
thus f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) by A2, A4, A5
.= f2 . (x,y) by A3, A4, A5 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
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] & 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 )
proof
let X, Y, Z, W be non empty MetrSpace; ::_thesis: 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 )
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]; ::_thesis: ( (dist_cart4 (X,Y,Z,W)) . (x,y) = 0 iff x = y )
reconsider x1 = x `1_4 , y1 = y `1_4 as Element of X ;
reconsider x2 = x `2_4 , y2 = y `2_4 as Element of Y ;
reconsider x3 = x `3_4 , y3 = y `3_4 as Element of Z ;
reconsider x4 = x `4_4 , y4 = y `4_4 as Element of W ;
A1: ( x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] ) by MCART_1:56;
thus  ( (dist_cart4 (X,Y,Z,W)) . (x,y) = 0 implies x = y ) ::_thesis: ( x = y implies (dist_cart4 (X,Y,Z,W)) . (x,y) = 0 )
proof
set d1 = dist (x1,y1);
set d2 = dist (x2,y2);
set d3 = dist (x3,y3);
set d5 = dist (x4,y4);
set d4 = (dist (x1,y1)) + (dist (x2,y2));
set d6 = (dist (x3,y3)) + (dist (x4,y4));
A2: ( 0 <= dist (x3,y3) & 0 <= dist (x4,y4) ) by METRIC_1:5;
then A3: 0 + 0 <= (dist (x3,y3)) + (dist (x4,y4)) by XREAL_1:7;
assume  (dist_cart4 (X,Y,Z,W)) . (x,y) = 0 ; ::_thesis: x = y
then A4: ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) = 0 by A1, Def7;
A5: ( 0 <= dist (x1,y1) & 0 <= dist (x2,y2) ) by METRIC_1:5;
then A6: 0 + 0 <= (dist (x1,y1)) + (dist (x2,y2)) by XREAL_1:7;
then A7: (dist (x1,y1)) + (dist (x2,y2)) = 0 by A4, A3, XREAL_1:27;
then  dist (x2,y2) = 0 by A5, XREAL_1:27;
then A8: x2 = y2 by METRIC_1:2;
A9: (dist (x3,y3)) + (dist (x4,y4)) = 0 by A4, A6, A3, XREAL_1:27;
then  dist (x3,y3) = 0 by A2, XREAL_1:27;
then A10: x3 = y3 by METRIC_1:2;
 dist (x4,y4) = 0 by A2, A9, XREAL_1:27;
then A11: x4 = y4 by METRIC_1:2;
 dist (x1,y1) = 0 by A5, A7, XREAL_1:27;
hence  x = y by A1, A8, A10, A11, METRIC_1:2; ::_thesis: verum
end;
assume A12: x = y ; ::_thesis: (dist_cart4 (X,Y,Z,W)) . (x,y) = 0
then A13: ( dist (x2,y2) = 0 & dist (x3,y3) = 0 ) by METRIC_1:1;
A14: dist (x4,y4) = 0 by A12, METRIC_1:1;
(dist_cart4 (X,Y,Z,W)) . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) by A1, Def7
.= 0 by A12, A13, A14, METRIC_1:1 ;
hence  (dist_cart4 (X,Y,Z,W)) . (x,y) = 0 ; ::_thesis: verum
end;

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)
proof
let X, Y, Z, W be non empty MetrSpace; ::_thesis: 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)
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]; ::_thesis: (dist_cart4 (X,Y,Z,W)) . (x,y) = (dist_cart4 (X,Y,Z,W)) . (y,x)
reconsider x1 = x `1_4 , y1 = y `1_4 as Element of X ;
reconsider x2 = x `2_4 , y2 = y `2_4 as Element of Y ;
reconsider x3 = x `3_4 , y3 = y `3_4 as Element of Z ;
reconsider x4 = x `4_4 , y4 = y `4_4 as Element of W ;
A1: ( x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] ) by MCART_1:56;
then (dist_cart4 (X,Y,Z,W)) . (x,y) = ((dist (y1,x1)) + (dist (y2,x2))) + ((dist (y3,x3)) + (dist (x4,y4))) by Def7
.= (dist_cart4 (X,Y,Z,W)) . (y,x) by A1, Def7 ;
hence  (dist_cart4 (X,Y,Z,W)) . (x,y) = (dist_cart4 (X,Y,Z,W)) . (y,x) ; ::_thesis: verum
end;

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))
proof
let X, Y, Z, W be non empty MetrSpace; ::_thesis: 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))
let x, y, z be Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]; ::_thesis: (dist_cart4 (X,Y,Z,W)) . (x,z) <= ((dist_cart4 (X,Y,Z,W)) . (x,y)) + ((dist_cart4 (X,Y,Z,W)) . (y,z))
reconsider x1 = x `1_4 , y1 = y `1_4 , z1 = z `1_4 as Element of X ;
reconsider x2 = x `2_4 , y2 = y `2_4 , z2 = z `2_4 as Element of Y ;
reconsider x3 = x `3_4 , y3 = y `3_4 , z3 = z `3_4 as Element of Z ;
reconsider x4 = x `4_4 , y4 = y `4_4 , z4 = z `4_4 as Element of W ;
A1: x = [x1,x2,x3,x4] by MCART_1:56;
set d7 = dist (x3,z3);
set d8 = dist (x3,y3);
set d9 = dist (y3,z3);
set d1 = dist (x1,z1);
set d2 = dist (x1,y1);
set d3 = dist (y1,z1);
A2: y = [y1,y2,y3,y4] by MCART_1:56;
set d10 = dist (x4,z4);
set d11 = dist (x4,y4);
set d12 = dist (y4,z4);
set d4 = dist (x2,z2);
set d5 = dist (x2,y2);
set d6 = dist (y2,z2);
A3: z = [z1,z2,z3,z4] by MCART_1:56;
set d16 = (dist (x3,z3)) + (dist (x4,z4));
set d14 = (dist (x1,z1)) + (dist (x2,z2));
set d17 = ((dist (x3,y3)) + (dist (y3,z3))) + ((dist (x4,y4)) + (dist (y4,z4)));
set d15 = ((dist (x1,y1)) + (dist (y1,z1))) + ((dist (x2,y2)) + (dist (y2,z2)));
 ( dist (x3,z3) <= (dist (x3,y3)) + (dist (y3,z3)) & dist (x4,z4) <= (dist (x4,y4)) + (dist (y4,z4)) ) by METRIC_1:4;
then A4: (dist (x3,z3)) + (dist (x4,z4)) <= ((dist (x3,y3)) + (dist (y3,z3))) + ((dist (x4,y4)) + (dist (y4,z4))) by XREAL_1:7;
 ( dist (x1,z1) <= (dist (x1,y1)) + (dist (y1,z1)) & dist (x2,z2) <= (dist (x2,y2)) + (dist (y2,z2)) ) by METRIC_1:4;
then  (dist (x1,z1)) + (dist (x2,z2)) <= ((dist (x1,y1)) + (dist (y1,z1))) + ((dist (x2,y2)) + (dist (y2,z2))) by XREAL_1:7;
then A5: ((dist (x1,z1)) + (dist (x2,z2))) + ((dist (x3,z3)) + (dist (x4,z4))) <= (((dist (x1,y1)) + (dist (y1,z1))) + ((dist (x2,y2)) + (dist (y2,z2)))) + (((dist (x3,y3)) + (dist (y3,z3))) + ((dist (x4,y4)) + (dist (y4,z4)))) by A4, XREAL_1:7;
(((dist (x1,y1)) + (dist (y1,z1))) + ((dist (x2,y2)) + (dist (y2,z2)))) + (((dist (x3,y3)) + (dist (y3,z3))) + ((dist (x4,y4)) + (dist (y4,z4)))) = (((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4)))) + (((dist (y1,z1)) + (dist (y2,z2))) + ((dist (y3,z3)) + (dist (y4,z4))))
.= ((dist_cart4 (X,Y,Z,W)) . (x,y)) + (((dist (y1,z1)) + (dist (y2,z2))) + ((dist (y3,z3)) + (dist (y4,z4)))) by A1, A2, Def7
.= ((dist_cart4 (X,Y,Z,W)) . (x,y)) + ((dist_cart4 (X,Y,Z,W)) . (y,z)) by A2, A3, Def7 ;
hence  (dist_cart4 (X,Y,Z,W)) . (x,z) <= ((dist_cart4 (X,Y,Z,W)) . (x,y)) + ((dist_cart4 (X,Y,Z,W)) . (y,z)) by A1, A3, A5, Def7; ::_thesis: verum
end;

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
proof
set M = MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],(dist_cart4 (X,Y,Z,W)) #);
now__::_thesis:_for_x,_y,_z_being_Element_of_MetrStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y,_the_carrier_of_Z,_the_carrier_of_W:],(dist_cart4_(X,Y,Z,W))_#)_holds_
(_(_dist_(x,y)_=_0_implies_x_=_y_)_&_(_x_=_y_implies_dist_(x,y)_=_0_)_&_dist_(x,y)_=_dist_(y,x)_&_dist_(x,z)_<=_(dist_(x,y))_+_(dist_(y,z))_)
let x, y, z be Element of MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],(dist_cart4 (X,Y,Z,W)) #); ::_thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
reconsider x9 = x, y9 = y, z9 = z as Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] ;
A1: dist (x,y) = (dist_cart4 (X,Y,Z,W)) . (x9,y9) by METRIC_1:def_1;
hence  ( dist (x,y) = 0 iff x = y ) by Th7; ::_thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
 dist (y,x) = (dist_cart4 (X,Y,Z,W)) . (y9,x9) by METRIC_1:def_1;
hence  dist (x,y) = dist (y,x) by A1, Th8; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
 ( dist (x,z) = (dist_cart4 (X,Y,Z,W)) . (x9,z9) & dist (y,z) = (dist_cart4 (X,Y,Z,W)) . (y9,z9) ) by METRIC_1:def_1;
hence  dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th9; ::_thesis: verum
end;
hence  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 by METRIC_1:6; ::_thesis: verum
end;
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] & 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] & y = [y1,y2] holds
b1 . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2))
proof
deffunc H1( Element of X, Element of X, Element of Y, Element of Y) ->  Element of REAL = sqrt (((dist ($1,$2)) ^2) + ((dist ($3,$4)) ^2));
consider F being Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL such that
A1: 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
F . (x,y) = H1(x1,y1,x2,y2) from METRIC_3:sch_1();
take  F ; ::_thesis: 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
F . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2))
let x1, y1 be Element of X; ::_thesis: 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
F . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2))
let x2, y2 be Element of Y; ::_thesis: for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
F . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2))
let x, y be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: ( x = [x1,x2] & y = [y1,y2] implies F . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) )
assume  ( x = [x1,x2] & y = [y1,y2] ) ; ::_thesis: F . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2))
hence  F . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) by A1; ::_thesis: verum
end;
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) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) ) & ( 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) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) ) holds
b1 = b2
proof
let f1, f2 be Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL; ::_thesis: ( ( 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
f1 . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) ) & ( 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
f2 . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) ) implies f1 = f2 )
assume that
A2: 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
f1 . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) and
A3: 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
f2 . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) ; ::_thesis: f1 = f2
 for x, y being Element of [: the carrier of X, the carrier of Y:] holds f1 . (x,y) = f2 . (x,y)
proof
let x, y be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: f1 . (x,y) = f2 . (x,y)
consider x1 being Element of X, x2 being Element of Y such that
A4: x = [x1,x2] by DOMAIN_1:1;
consider y1 being Element of X, y2 being Element of Y such that
A5: y = [y1,y2] by DOMAIN_1:1;
thus f1 . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) by A2, A4, A5
.= f2 . (x,y) by A3, A4, A5 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
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] & 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 & 0 <= b holds
( sqrt (a + b) = 0 iff ( a = 0 & 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 )
proof
let X, Y be non empty MetrSpace; ::_thesis: 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 )
let x, y be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: ( (dist_cart2S (X,Y)) . (x,y) = 0 iff x = y )
reconsider x1 = x `1 , y1 = y `1 as Element of X ;
reconsider x2 = x `2 , y2 = y `2 as Element of Y ;
A1: ( x = [x1,x2] & y = [y1,y2] ) by MCART_1:22;
thus  ( (dist_cart2S (X,Y)) . (x,y) = 0 implies x = y ) ::_thesis: ( x = y implies (dist_cart2S (X,Y)) . (x,y) = 0 )
proof
set d2 = dist (x2,y2);
set d1 = dist (x1,y1);
assume  (dist_cart2S (X,Y)) . (x,y) = 0 ; ::_thesis: x = y
then A2: sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) = 0 by A1, Def10;
A3: ( 0 <= (dist (x1,y1)) ^2 & 0 <= (dist (x2,y2)) ^2 ) by XREAL_1:63;
then  dist (x1,y1) = 0 by A2, Lm1;
then A4: x1 = y1 by METRIC_1:2;
 dist (x2,y2) = 0 by A2, A3, Lm1;
hence  x = y by A1, A4, METRIC_1:2; ::_thesis: verum
end;
assume  x = y ; ::_thesis: (dist_cart2S (X,Y)) . (x,y) = 0
then A5: ( (dist (x1,y1)) ^2 = 0 ^2 & (dist (x2,y2)) ^2 = 0 ^2 ) by METRIC_1:1;
(dist_cart2S (X,Y)) . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) by A1, Def10
.= 0 by A5, Lm1 ;
hence  (dist_cart2S (X,Y)) . (x,y) = 0 ; ::_thesis: verum
end;

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)
proof
let X, Y be non empty MetrSpace; ::_thesis: 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)
let x, y be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: (dist_cart2S (X,Y)) . (x,y) = (dist_cart2S (X,Y)) . (y,x)
reconsider x1 = x `1 , y1 = y `1 as Element of X ;
reconsider x2 = x `2 , y2 = y `2 as Element of Y ;
A1: ( x = [x1,x2] & y = [y1,y2] ) by MCART_1:22;
then (dist_cart2S (X,Y)) . (x,y) = sqrt (((dist (y1,x1)) ^2) + ((dist (x2,y2)) ^2)) by Def10
.= (dist_cart2S (X,Y)) . (y,x) by A1, Def10 ;
hence  (dist_cart2S (X,Y)) . (x,y) = (dist_cart2S (X,Y)) . (y,x) ; ::_thesis: verum
end;

theorem Th12: :: METRIC_3:12
for a, b, c, d being real number st 0 <= a & 0 <= b & 0 <= c & 0 <= d holds
sqrt (((a + c) ^2) + ((b + d) ^2)) <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2)))
proof
let a, b, c, d be real number ; ::_thesis: ( 0 <= a & 0 <= b & 0 <= c & 0 <= d implies sqrt (((a + c) ^2) + ((b + d) ^2)) <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2))) )
assume  ( 0 <= a & 0 <= b & 0 <= c & 0 <= d ) ; ::_thesis: sqrt (((a + c) ^2) + ((b + d) ^2)) <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2)))
then  ( 0 <= a * c & 0 <= d * b ) by XREAL_1:127;
then A1: 0 + 0 <= (a * c) + (d * b) by XREAL_1:7;
 ( 0 <= d ^2 & 0 <= c ^2 ) by XREAL_1:63;
then A2: 0 + 0 <= (c ^2) + (d ^2) by XREAL_1:7;
then A3: 0 <= sqrt ((c ^2) + (d ^2)) by SQUARE_1:def_2;
 0 <= ((a * d) - (c * b)) ^2 by XREAL_1:63;
then  0 <= (((a ^2) * (d ^2)) + ((c ^2) * (b ^2))) - ((2 * (a * d)) * (c * b)) ;
then  0 + ((2 * (a * d)) * (c * b)) <= ((a ^2) * (d ^2)) + ((c ^2) * (b ^2)) by XREAL_1:19;
then  ((b ^2) * (d ^2)) + ((2 * (a * d)) * (c * b)) <= (((a ^2) * (d ^2)) + ((c ^2) * (b ^2))) + ((b ^2) * (d ^2)) by XREAL_1:6;
then A4: ((a ^2) * (c ^2)) + (((b ^2) * (d ^2)) + ((2 * (a * d)) * (c * b))) <= ((a ^2) * (c ^2)) + (((b ^2) * (d ^2)) + (((a ^2) * (d ^2)) + ((c ^2) * (b ^2)))) by XREAL_1:6;
 ( 0 <= a ^2 & 0 <= b ^2 ) by XREAL_1:63;
then A5: 0 + 0 <= (a ^2) + (b ^2) by XREAL_1:7;
then  0 <= sqrt ((a ^2) + (b ^2)) by SQUARE_1:def_2;
then A6: 0 + 0 <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2))) by A3, XREAL_1:7;
 0 <= ((a * c) + (d * b)) ^2 by XREAL_1:63;
then  sqrt (((a * c) + (d * b)) ^2) <= sqrt (((a ^2) + (b ^2)) * ((c ^2) + (d ^2))) by A4, SQUARE_1:26;
then  2 * (sqrt (((a * c) + (d * b)) ^2)) <= 2 * (sqrt (((a ^2) + (b ^2)) * ((c ^2) + (d ^2)))) by XREAL_1:64;
then  2 * (sqrt (((a * c) + (d * b)) ^2)) <= 2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((c ^2) + (d ^2)))) by A5, A2, SQUARE_1:29;
then  2 * ((a * c) + (d * b)) <= 2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((d ^2) + (c ^2)))) by A1, SQUARE_1:22;
then  (b ^2) + (2 * ((a * c) + (d * b))) <= (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((d ^2) + (c ^2))))) + (b ^2) by XREAL_1:6;
then  (d ^2) + ((b ^2) + (2 * ((a * c) + (d * b)))) <= (d ^2) + ((b ^2) + (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((d ^2) + (c ^2)))))) by XREAL_1:6;
then  (c ^2) + ((d ^2) + ((b ^2) + (2 * ((a * c) + (d * b))))) <= ((d ^2) + ((b ^2) + (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((d ^2) + (c ^2))))))) + (c ^2) by XREAL_1:6;
then  (a ^2) + ((c ^2) + ((d ^2) + (((b ^2) + (2 * (d * b))) + (2 * (a * c))))) <= (a ^2) + ((c ^2) + ((d ^2) + ((b ^2) + (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((d ^2) + (c ^2)))))))) by XREAL_1:6;
then  ((a + c) ^2) + ((d + b) ^2) <= (((a ^2) + (b ^2)) + (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((c ^2) + (d ^2)))))) + ((c ^2) + (d ^2)) ;
then  ((a + c) ^2) + ((d + b) ^2) <= (((sqrt ((a ^2) + (b ^2))) ^2) + (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((c ^2) + (d ^2)))))) + ((c ^2) + (d ^2)) by A5, SQUARE_1:def_2;
then A7: ((a + c) ^2) + ((d + b) ^2) <= (((sqrt ((a ^2) + (b ^2))) ^2) + ((2 * (sqrt ((a ^2) + (b ^2)))) * (sqrt ((c ^2) + (d ^2))))) + ((sqrt ((c ^2) + (d ^2))) ^2) by A2, SQUARE_1:def_2;
 ( 0 <= (a + c) ^2 & 0 <= (d + b) ^2 ) by XREAL_1:63;
then  0 + 0 <= ((a + c) ^2) + ((d + b) ^2) by XREAL_1:7;
then  sqrt (((a + c) ^2) + ((d + b) ^2)) <= sqrt (((sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2)))) ^2) by A7, SQUARE_1:26;
hence  sqrt (((a + c) ^2) + ((b + d) ^2)) <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2))) by A6, SQUARE_1:22; ::_thesis: verum
end;

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))
proof
let X, Y be non empty MetrSpace; ::_thesis: 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))
let x, y, z be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: (dist_cart2S (X,Y)) . (x,z) <= ((dist_cart2S (X,Y)) . (x,y)) + ((dist_cart2S (X,Y)) . (y,z))
reconsider x1 = x `1 , y1 = y `1 , z1 = z `1 as Element of X ;
reconsider x2 = x `2 , y2 = y `2 , z2 = z `2 as Element of Y ;
A1: x = [x1,x2] by MCART_1:22;
set d5 = dist (x2,y2);
set d3 = dist (y1,z1);
set d1 = dist (x1,z1);
A2: y = [y1,y2] by MCART_1:22;
set d6 = dist (y2,z2);
set d4 = dist (x2,z2);
set d2 = dist (x1,y1);
A3: z = [z1,z2] by MCART_1:22;
 ( 0 <= (dist (x1,z1)) ^2 & 0 <= (dist (x2,z2)) ^2 ) by XREAL_1:63;
then A4: 0 + 0 <= ((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2) by XREAL_1:7;
 ( dist (x2,z2) <= (dist (x2,y2)) + (dist (y2,z2)) & 0 <= dist (x2,z2) ) by METRIC_1:4, METRIC_1:5;
then A5: (dist (x2,z2)) ^2 <= ((dist (x2,y2)) + (dist (y2,z2))) ^2 by SQUARE_1:15;
 ( dist (x1,z1) <= (dist (x1,y1)) + (dist (y1,z1)) & 0 <= dist (x1,z1) ) by METRIC_1:4, METRIC_1:5;
then  (dist (x1,z1)) ^2 <= ((dist (x1,y1)) + (dist (y1,z1))) ^2 by SQUARE_1:15;
then  ((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2) <= (((dist (x1,y1)) + (dist (y1,z1))) ^2) + (((dist (x2,y2)) + (dist (y2,z2))) ^2) by A5, XREAL_1:7;
then A6: sqrt (((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2)) <= sqrt ((((dist (x1,y1)) + (dist (y1,z1))) ^2) + (((dist (x2,y2)) + (dist (y2,z2))) ^2)) by A4, SQUARE_1:26;
A7: ( 0 <= dist (x2,y2) & 0 <= dist (y2,z2) ) by METRIC_1:5;
 ( 0 <= dist (x1,y1) & 0 <= dist (y1,z1) ) by METRIC_1:5;
then  sqrt ((((dist (x1,y1)) + (dist (y1,z1))) ^2) + (((dist (x2,y2)) + (dist (y2,z2))) ^2)) <= (sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2))) + (sqrt (((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2))) by A7, Th12;
then  sqrt (((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2)) <= (sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2))) + (sqrt (((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2))) by A6, XXREAL_0:2;
then  (dist_cart2S (X,Y)) . (x,z) <= (sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2))) + (sqrt (((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2))) by A1, A3, Def10;
then  (dist_cart2S (X,Y)) . (x,z) <= ((dist_cart2S (X,Y)) . (x,y)) + (sqrt (((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2))) by A1, A2, Def10;
hence  (dist_cart2S (X,Y)) . (x,z) <= ((dist_cart2S (X,Y)) . (x,y)) + ((dist_cart2S (X,Y)) . (y,z)) by A2, A3, Def10; ::_thesis: verum
end;

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
proof
now__::_thesis:_for_x,_y,_z_being_Element_of_MetrStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],(dist_cart2S_(X,Y))_#)_holds_
(_(_dist_(x,y)_=_0_implies_x_=_y_)_&_(_x_=_y_implies_dist_(x,y)_=_0_)_&_dist_(x,y)_=_dist_(y,x)_&_dist_(x,z)_<=_(dist_(x,y))_+_(dist_(y,z))_)
let x, y, z be Element of MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #); ::_thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
reconsider x9 = x, y9 = y, z9 = z as Element of [: the carrier of X, the carrier of Y:] ;
A1: dist (x,y) = (dist_cart2S (X,Y)) . (x9,y9) by METRIC_1:def_1;
hence  ( dist (x,y) = 0 iff x = y ) by Th10; ::_thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
 dist (y,x) = (dist_cart2S (X,Y)) . (y9,x9) by METRIC_1:def_1;
hence  dist (x,y) = dist (y,x) by A1, Th11; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
 ( dist (x,z) = (dist_cart2S (X,Y)) . (x9,z9) & dist (y,z) = (dist_cart2S (X,Y)) . (y9,z9) ) by METRIC_1:def_1;
hence  dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th13; ::_thesis: verum
end;
hence  MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #) is non empty strict MetrSpace by METRIC_1:6; ::_thesis: verum
end;
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] & 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] & y = [y1,y2,y3] holds
b1 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))
proof
deffunc H1( Element of X, Element of X, Element of Y, Element of Y, Element of Z, Element of Z) ->  Element of REAL = sqrt ((((dist ($1,$2)) ^2) + ((dist ($3,$4)) ^2)) + ((dist ($5,$6)) ^2));
consider F 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 such that
A1: 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] & y = [y1,y2,y3] holds
F . (x,y) = H1(x1,y1,x2,y2,x3,y3) from METRIC_3:sch_2();
take  F ; ::_thesis: 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] & y = [y1,y2,y3] holds
F . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))
let x1, y1 be Element of X; ::_thesis: 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] & y = [y1,y2,y3] holds
F . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))
let x2, y2 be Element of Y; ::_thesis: 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] & y = [y1,y2,y3] holds
F . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))
let x3, y3 be Element of Z; ::_thesis: for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
F . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; ::_thesis: ( x = [x1,x2,x3] & y = [y1,y2,y3] implies F . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) )
assume  ( x = [x1,x2,x3] & y = [y1,y2,y3] ) ; ::_thesis: F . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))
hence  F . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) by A1; ::_thesis: verum
end;
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] & y = [y1,y2,y3] holds
b1 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) ) & ( 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] & y = [y1,y2,y3] holds
b2 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) ) holds
b1 = b2
proof
let f1, f2 be 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; ::_thesis: ( ( 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] & y = [y1,y2,y3] holds
f1 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) ) & ( 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] & y = [y1,y2,y3] holds
f2 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) ) implies f1 = f2 )
assume that
A2: 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] & y = [y1,y2,y3] holds
f1 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) and
A3: 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] & y = [y1,y2,y3] holds
f2 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) ; ::_thesis: f1 = f2
 for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds f1 . (x,y) = f2 . (x,y)
proof
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; ::_thesis: f1 . (x,y) = f2 . (x,y)
consider x1 being Element of X, x2 being Element of Y, x3 being Element of Z such that
A4: x = [x1,x2,x3] by DOMAIN_1:3;
consider y1 being Element of X, y2 being Element of Y, y3 being Element of Z such that
A5: y = [y1,y2,y3] by DOMAIN_1:3;
thus f1 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) by A2, A4, A5
.= f2 . (x,y) by A3, A4, A5 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
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] & 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 )
proof
let X, Y, Z be non empty MetrSpace; ::_thesis: 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 )
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; ::_thesis: ( (dist_cart3S (X,Y,Z)) . (x,y) = 0 iff x = y )
reconsider x1 = x `1_3 , y1 = y `1_3 as Element of X ;
reconsider x2 = x `2_3 , y2 = y `2_3 as Element of Y ;
reconsider x3 = x `3_3 , y3 = y `3_3 as Element of Z ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) by MCART_1:44;
thus  ( (dist_cart3S (X,Y,Z)) . (x,y) = 0 implies x = y ) ::_thesis: ( x = y implies (dist_cart3S (X,Y,Z)) . (x,y) = 0 )
proof
set d3 = dist (x3,y3);
set d2 = dist (x2,y2);
set d1 = dist (x1,y1);
A2: ( 0 <= (dist (x2,y2)) ^2 & 0 <= (dist (x3,y3)) ^2 ) by XREAL_1:63;
assume  (dist_cart3S (X,Y,Z)) . (x,y) = 0 ; ::_thesis: x = y
then  sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) = 0 by A1, Def13;
then A3: sqrt (((dist (x1,y1)) ^2) + (((dist (x2,y2)) ^2) + ((dist (x3,y3)) ^2))) = 0 ;
 ( 0 <= (dist (x2,y2)) ^2 & 0 <= (dist (x3,y3)) ^2 ) by XREAL_1:63;
then A4: ( 0 <= (dist (x1,y1)) ^2 & 0 + 0 <= ((dist (x2,y2)) ^2) + ((dist (x3,y3)) ^2) ) by XREAL_1:7, XREAL_1:63;
then  dist (x1,y1) = 0 by A3, Lm1;
then A5: x1 = y1 by METRIC_1:2;
A6: ((dist (x2,y2)) ^2) + ((dist (x3,y3)) ^2) = 0 by A3, A4, Lm1;
then  dist (x2,y2) = 0 by A2, XREAL_1:27;
then A7: x2 = y2 by METRIC_1:2;
 dist (x3,y3) = 0 by A6, A2, XREAL_1:27;
hence  x = y by A1, A5, A7, METRIC_1:2; ::_thesis: verum
end;
assume A8: x = y ; ::_thesis: (dist_cart3S (X,Y,Z)) . (x,y) = 0
then A9: ( (dist (x1,y1)) ^2 = 0 ^2 & (dist (x2,y2)) ^2 = 0 ^2 ) by METRIC_1:1;
(dist_cart3S (X,Y,Z)) . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) by A1, Def13
.= 0 ^2 by A8, A9, METRIC_1:1, SQUARE_1:17 ;
hence  (dist_cart3S (X,Y,Z)) . (x,y) = 0 ; ::_thesis: verum
end;

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)
proof
let X, Y, Z be non empty MetrSpace; ::_thesis: 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)
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; ::_thesis: (dist_cart3S (X,Y,Z)) . (x,y) = (dist_cart3S (X,Y,Z)) . (y,x)
reconsider x1 = x `1_3 , y1 = y `1_3 as Element of X ;
reconsider x2 = x `2_3 , y2 = y `2_3 as Element of Y ;
reconsider x3 = x `3_3 , y3 = y `3_3 as Element of Z ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) by MCART_1:44;
then (dist_cart3S (X,Y,Z)) . (x,y) = sqrt ((((dist (y1,x1)) ^2) + ((dist (y2,x2)) ^2)) + ((dist (y3,x3)) ^2)) by Def13
.= (dist_cart3S (X,Y,Z)) . (y,x) by A1, Def13 ;
hence  (dist_cart3S (X,Y,Z)) . (x,y) = (dist_cart3S (X,Y,Z)) . (y,x) ; ::_thesis: verum
end;

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)
proof
let a, b, c, d, e, f be real number ; ::_thesis: (((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)
 ( 0 <= ((a * f) - (e * c)) ^2 & 0 <= ((b * f) - (e * d)) ^2 ) by XREAL_1:63;
then  ( 0 <= ((a * d) - (c * b)) ^2 & 0 + 0 <= (((a * f) - (e * c)) ^2) + (((b * f) - (e * d)) ^2) ) by XREAL_1:7, XREAL_1:63;
then  0 + 0 <= (((a * d) - (c * b)) ^2) + ((((a * f) - (e * c)) ^2) + (((b * f) - (e * d)) ^2)) by XREAL_1:7;
then  0 <= (((((a * d) ^2) + ((c * b) ^2)) + (((a * f) - (e * c)) ^2)) + (((b * f) - (e * d)) ^2)) - ((2 * (a * d)) * (c * b)) ;
then  0 + ((2 * (a * d)) * (c * b)) <= ((((a * d) ^2) + ((c * b) ^2)) + (((a * f) - (e * c)) ^2)) + (((b * f) - (e * d)) ^2) by XREAL_1:19;
then  (2 * (a * d)) * (c * b) <= ((((((a * d) ^2) + ((c * b) ^2)) + ((a * f) ^2)) + ((e * c) ^2)) + (((b * f) - (e * d)) ^2)) - ((2 * (a * f)) * (e * c)) ;
then  ((2 * (a * d)) * (c * b)) + ((2 * (a * f)) * (e * c)) <= (((((((a * d) ^2) + ((c * b) ^2)) + ((a * f) ^2)) + ((e * c) ^2)) + ((b * f) ^2)) + ((e * d) ^2)) - ((2 * (b * f)) * (e * d)) by XREAL_1:19;
hence  (((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) by XREAL_1:19; ::_thesis: verum
end;

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))
proof
let a, b, c, d, e, f be real number ; ::_thesis: (((a * c) + (b * d)) + (e * f)) ^2 <= (((a ^2) + (b ^2)) + (e ^2)) * (((c ^2) + (d ^2)) + (f ^2))
 (((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) by Th16;
then  ((e * f) ^2) + ((((2 * (a * b)) * (c * d)) + ((2 * (a * c)) * (e * f))) + ((2 * (b * d)) * (e * f))) <= (((((((a * d) ^2) + ((c * b) ^2)) + ((a * f) ^2)) + ((e * c) ^2)) + ((b * f) ^2)) + ((e * d) ^2)) + ((e * f) ^2) by XREAL_1:6;
then  ((b * d) ^2) + (((e * f) ^2) + ((((2 * (a * b)) * (c * d)) + ((2 * (a * c)) * (e * f))) + ((2 * (b * d)) * (e * f)))) <= ((((((((a * d) ^2) + ((c * b) ^2)) + ((a * f) ^2)) + ((e * c) ^2)) + ((b * f) ^2)) + ((e * d) ^2)) + ((e * f) ^2)) + ((b * d) ^2) by XREAL_1:6;
then  ((a * c) ^2) + (((b * d) ^2) + (((e * f) ^2) + ((((2 * (a * b)) * (c * d)) + ((2 * (a * c)) * (e * f))) + ((2 * (b * d)) * (e * f))))) <= (((((((((a * d) ^2) + ((c * b) ^2)) + ((a * f) ^2)) + ((e * c) ^2)) + ((b * f) ^2)) + ((e * d) ^2)) + ((e * f) ^2)) + ((b * d) ^2)) + ((a * c) ^2) by XREAL_1:6;
hence  (((a * c) + (b * d)) + (e * f)) ^2 <= (((a ^2) + (b ^2)) + (e ^2)) * (((c ^2) + (d ^2)) + (f ^2)) ; ::_thesis: verum
end;

Lm2:  for a, b, c, d, e, f being real number st 0 <= a & 0 <= b & 0 <= c & 0 <= d & 0 <= e & 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)))
proof
let a, b, c, d, e, f be real number ; ::_thesis: ( 0 <= a & 0 <= b & 0 <= c & 0 <= d & 0 <= e & 0 <= f implies sqrt ((((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2)) <= (sqrt (((a ^2) + (b ^2)) + (e ^2))) + (sqrt (((c ^2) + (d ^2)) + (f ^2))) )
assume that
A1: 0 <= a and
A2: 0 <= b and
A3: 0 <= c and
A4: ( 0 <= d & 0 <= e & 0 <= f ) ; ::_thesis: sqrt ((((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2)) <= (sqrt (((a ^2) + (b ^2)) + (e ^2))) + (sqrt (((c ^2) + (d ^2)) + (f ^2)))
 ( 0 <= b * d & 0 <= e * f ) by A2, A4, XREAL_1:127;
then A5: 0 + 0 <= (b * d) + (e * f) by XREAL_1:7;
 ( 0 <= c ^2 & 0 <= d ^2 ) by XREAL_1:63;
then A6: 0 + 0 <= (c ^2) + (d ^2) by XREAL_1:7;
 0 <= f ^2 by XREAL_1:63;
then A7: 0 + 0 <= ((c ^2) + (d ^2)) + (f ^2) by A6, XREAL_1:7;
then A8: 0 <= sqrt (((c ^2) + (d ^2)) + (f ^2)) by SQUARE_1:def_2;
 0 <= (((a * c) + (b * d)) + (e * f)) ^2 by XREAL_1:63;
then A9: sqrt ((((a * c) + (b * d)) + (e * f)) ^2) <= sqrt ((((a ^2) + (b ^2)) + (e ^2)) * (((c ^2) + (d ^2)) + (f ^2))) by Th17, SQUARE_1:26;
 ( 0 <= a ^2 & 0 <= b ^2 ) by XREAL_1:63;
then A10: 0 + 0 <= (a ^2) + (b ^2) by XREAL_1:7;
 0 <= e ^2 by XREAL_1:63;
then A11: 0 + 0 <= ((a ^2) + (b ^2)) + (e ^2) by A10, XREAL_1:7;
 0 <= a * c by A1, A3, XREAL_1:127;
then  0 + 0 <= (a * c) + ((b * d) + (e * f)) by A5, XREAL_1:7;
then  ((a * c) + (b * d)) + (e * f) <= sqrt ((((a ^2) + (b ^2)) + (e ^2)) * (((c ^2) + (d ^2)) + (f ^2))) by A9, SQUARE_1:22;
then  ((a * c) + (b * d)) + (e * f) <= (sqrt (((a ^2) + (b ^2)) + (e ^2))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))) by A11, A7, SQUARE_1:29;
then  2 * (((a * c) + (b * d)) + (e * f)) <= 2 * ((sqrt (((a ^2) + (b ^2)) + (e ^2))) * (sqrt (((c ^2) + (d ^2)) + (f ^2)))) by XREAL_1:64;
then  ((2 * ((a * c) + (b * d))) + (2 * (e * f))) + (e ^2) <= ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2)))) + (e ^2) by XREAL_1:6;
then  ((2 * ((a * c) + (b * d))) + ((e ^2) + (2 * (e * f)))) + (f ^2) <= (((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2)))) + (e ^2)) + (f ^2) by XREAL_1:6;
then  (((2 * (a * c)) + (2 * (b * d))) + ((e + f) ^2)) + (b ^2) <= (((e ^2) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + (f ^2)) + (b ^2) by XREAL_1:6;
then  (((2 * (a * c)) + ((b ^2) + (2 * (b * d)))) + ((e + f) ^2)) + (d ^2) <= ((b ^2) + (((e ^2) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + (f ^2))) + (d ^2) by XREAL_1:6;
then  (a ^2) + ((2 * (a * c)) + (((b + d) ^2) + ((e + f) ^2))) <= ((b ^2) + (((e ^2) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + ((d ^2) + (f ^2)))) + (a ^2) by XREAL_1:6;
then  (((a ^2) + (2 * (a * c))) + (((b + d) ^2) + ((e + f) ^2))) + (c ^2) <= (((((a ^2) + (b ^2)) + (e ^2)) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + ((d ^2) + (f ^2))) + (c ^2) by XREAL_1:6;
then  (((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2) <= ((((a ^2) + (b ^2)) + (e ^2)) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + ((c ^2) + ((d ^2) + (f ^2))) ;
then  (((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2) <= (((sqrt (((a ^2) + (b ^2)) + (e ^2))) ^2) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + (((c ^2) + (d ^2)) + (f ^2)) by A11, SQUARE_1:def_2;
then A12: (((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2) <= (((sqrt (((a ^2) + (b ^2)) + (e ^2))) ^2) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + ((sqrt (((c ^2) + (d ^2)) + (f ^2))) ^2) by A7, SQUARE_1:def_2;
 ( 0 <= (a + c) ^2 & 0 <= (b + d) ^2 ) by XREAL_1:63;
then A13: 0 + 0 <= ((a + c) ^2) + ((b + d) ^2) by XREAL_1:7;
 0 <= (e + f) ^2 by XREAL_1:63;
then  0 + 0 <= (((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2) by A13, XREAL_1:7;
then A14: sqrt ((((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2)) <= sqrt (((sqrt (((a ^2) + (b ^2)) + (e ^2))) + (sqrt (((c ^2) + (d ^2)) + (f ^2)))) ^2) by A12, SQUARE_1:26;
 0 <= sqrt (((a ^2) + (b ^2)) + (e ^2)) by A11, SQUARE_1:def_2;
then  0 + 0 <= (sqrt (((a ^2) + (b ^2)) + (e ^2))) + (sqrt (((c ^2) + (d ^2)) + (f ^2))) by A8, XREAL_1:7;
hence  sqrt ((((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2)) <= (sqrt (((a ^2) + (b ^2)) + (e ^2))) + (sqrt (((c ^2) + (d ^2)) + (f ^2))) by A14, SQUARE_1:22; ::_thesis: verum
end;

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))
proof
let X, Y, Z be non empty MetrSpace; ::_thesis: 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))
let x, y, z be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; ::_thesis: (dist_cart3S (X,Y,Z)) . (x,z) <= ((dist_cart3S (X,Y,Z)) . (x,y)) + ((dist_cart3S (X,Y,Z)) . (y,z))
reconsider x1 = x `1_3 , y1 = y `1_3 , z1 = z `1_3 as Element of X ;
reconsider x2 = x `2_3 , y2 = y `2_3 , z2 = z `2_3 as Element of Y ;
reconsider x3 = x `3_3 , y3 = y `3_3 , z3 = z `3_3 as Element of Z ;
A1: x = [x1,x2,x3] by MCART_1:44;
set d7 = dist (x3,z3);
set d8 = dist (x3,y3);
set d9 = dist (y3,z3);
set d1 = dist (x1,z1);
set d2 = dist (x1,y1);
set d3 = dist (y1,z1);
A2: y = [y1,y2,y3] by MCART_1:44;
 ( dist (x3,z3) <= (dist (x3,y3)) + (dist (y3,z3)) & 0 <= dist (x3,z3) ) by METRIC_1:4, METRIC_1:5;
then A3: (dist (x3,z3)) ^2 <= ((dist (x3,y3)) + (dist (y3,z3))) ^2 by SQUARE_1:15;
A4: ( 0 <= dist (x3,y3) & 0 <= dist (y3,z3) ) by METRIC_1:5;
set d4 = dist (x2,z2);
set d5 = dist (x2,y2);
set d6 = dist (y2,z2);
A5: z = [z1,z2,z3] by MCART_1:44;
 ( dist (x2,z2) <= (dist (x2,y2)) + (dist (y2,z2)) & 0 <= dist (x2,z2) ) by METRIC_1:4, METRIC_1:5;
then A6: (dist (x2,z2)) ^2 <= ((dist (x2,y2)) + (dist (y2,z2))) ^2 by SQUARE_1:15;
A7: ( 0 <= dist (x2,y2) & 0 <= dist (y2,z2) ) by METRIC_1:5;
 ( 0 <= (dist (x1,z1)) ^2 & 0 <= (dist (x2,z2)) ^2 ) by XREAL_1:63;
then A8: 0 + 0 <= ((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2) by XREAL_1:7;
 ( dist (x1,z1) <= (dist (x1,y1)) + (dist (y1,z1)) & 0 <= dist (x1,z1) ) by METRIC_1:4, METRIC_1:5;
then  (dist (x1,z1)) ^2 <= ((dist (x1,y1)) + (dist (y1,z1))) ^2 by SQUARE_1:15;
then  ((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2) <= (((dist (x1,y1)) + (dist (y1,z1))) ^2) + (((dist (x2,y2)) + (dist (y2,z2))) ^2) by A6, XREAL_1:7;
then A9: (((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2)) + ((dist (x3,z3)) ^2) <= ((((dist (x1,y1)) + (dist (y1,z1))) ^2) + (((dist (x2,y2)) + (dist (y2,z2))) ^2)) + (((dist (x3,y3)) + (dist (y3,z3))) ^2) by A3, XREAL_1:7;
 0 <= (dist (x3,z3)) ^2 by XREAL_1:63;
then  0 + 0 <= (((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2)) + ((dist (x3,z3)) ^2) by A8, XREAL_1:7;
then A10: sqrt ((((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2)) + ((dist (x3,z3)) ^2)) <= sqrt (((((dist (x1,y1)) + (dist (y1,z1))) ^2) + (((dist (x2,y2)) + (dist (y2,z2))) ^2)) + (((dist (x3,y3)) + (dist (y3,z3))) ^2)) by A9, SQUARE_1:26;
 ( 0 <= dist (x1,y1) & 0 <= dist (y1,z1) ) by METRIC_1:5;
then  sqrt (((((dist (x1,y1)) + (dist (y1,z1))) ^2) + (((dist (x2,y2)) + (dist (y2,z2))) ^2)) + (((dist (x3,y3)) + (dist (y3,z3))) ^2)) <= (sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))) + (sqrt ((((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2)) + ((dist (y3,z3)) ^2))) by A7, A4, Lm2;
then  sqrt ((((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2)) + ((dist (x3,z3)) ^2)) <= (sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))) + (sqrt ((((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2)) + ((dist (y3,z3)) ^2))) by A10, XXREAL_0:2;
then  (dist_cart3S (X,Y,Z)) . (x,z) <= (sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))) + (sqrt ((((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2)) + ((dist (y3,z3)) ^2))) by A1, A5, Def13;
then  (dist_cart3S (X,Y,Z)) . (x,z) <= ((dist_cart3S (X,Y,Z)) . (x,y)) + (sqrt ((((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2)) + ((dist (y3,z3)) ^2))) by A1, A2, Def13;
hence  (dist_cart3S (X,Y,Z)) . (x,z) <= ((dist_cart3S (X,Y,Z)) . (x,y)) + ((dist_cart3S (X,Y,Z)) . (y,z)) by A2, A5, Def13; ::_thesis: verum
end;

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
proof
now__::_thesis:_for_x,_y,_z_being_Element_of_MetrStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y,_the_carrier_of_Z:],(dist_cart3S_(X,Y,Z))_#)_holds_
(_(_dist_(x,y)_=_0_implies_x_=_y_)_&_(_x_=_y_implies_dist_(x,y)_=_0_)_&_dist_(x,y)_=_dist_(y,x)_&_dist_(x,z)_<=_(dist_(x,y))_+_(dist_(y,z))_)
let x, y, z be Element of MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3S (X,Y,Z)) #); ::_thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
reconsider x9 = x, y9 = y, z9 = z as Element of [: the carrier of X, the carrier of Y, the carrier of Z:] ;
A1: dist (x,y) = (dist_cart3S (X,Y,Z)) . (x9,y9) by METRIC_1:def_1;
hence  ( dist (x,y) = 0 iff x = y ) by Th14; ::_thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
 dist (y,x) = (dist_cart3S (X,Y,Z)) . (y9,x9) by METRIC_1:def_1;
hence  dist (x,y) = dist (y,x) by A1, Th15; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
 ( dist (x,z) = (dist_cart3S (X,Y,Z)) . (x9,z9) & dist (y,z) = (dist_cart3S (X,Y,Z)) . (y9,z9) ) by METRIC_1:def_1;
hence  dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th18; ::_thesis: verum
end;
hence  MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3S (X,Y,Z)) #) is non empty strict MetrSpace by METRIC_1:6; ::_thesis: verum
end;
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] & 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] & y = [y1,y2] holds
b1 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2))
proof
deffunc H1( Element of REAL , Element of REAL , Element of REAL , Element of REAL ) ->  Element of REAL = (real_dist . ($1,$2)) + (real_dist . ($3,$4));
consider F being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL such that
A1: for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
F . (x,y) = H1(x1,y1,x2,y2) from METRIC_3:sch_1();
take  F ; ::_thesis: for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
F . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2))
let x1, y1, x2, y2 be Element of REAL ; ::_thesis: for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
F . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2))
let x, y be Element of [:REAL,REAL:]; ::_thesis: ( x = [x1,x2] & y = [y1,y2] implies F . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) )
assume  ( x = [x1,x2] & y = [y1,y2] ) ; ::_thesis: F . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2))
hence  F . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) by A1; ::_thesis: verum
end;
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] & y = [y1,y2] holds
b1 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) ) & ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
b2 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) ) holds
b1 = b2
proof
let f1, f2 be Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL; ::_thesis: ( ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
f1 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) ) & ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
f2 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) ) implies f1 = f2 )
assume that
A2: for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
f1 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) and
A3: for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
f2 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) ; ::_thesis: f1 = f2
 for x, y being Element of [:REAL,REAL:] holds f1 . (x,y) = f2 . (x,y)
proof
let x, y be Element of [:REAL,REAL:]; ::_thesis: f1 . (x,y) = f2 . (x,y)
consider x1, x2 being Element of REAL  such that
A4: x = [x1,x2] by DOMAIN_1:1;
consider y1, y2 being Element of REAL  such that
A5: y = [y1,y2] by DOMAIN_1:1;
thus f1 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) by A2, A4, A5
.= f2 . (x,y) by A3, A4, A5 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
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] & 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 )
proof
let x, y be Element of [:REAL,REAL:]; ::_thesis: ( taxi_dist2 . (x,y) = 0 iff x = y )
reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 as Element of REAL ;
A1: ( x = [x1,x2] & y = [y1,y2] ) by MCART_1:22;
thus  ( taxi_dist2 . (x,y) = 0 implies x = y ) ::_thesis: ( x = y implies taxi_dist2 . (x,y) = 0 )
proof
set d2 = real_dist . (x2,y2);
set d1 = real_dist . (x1,y1);
 real_dist . (x1,y1) = abs (x1 - y1) by METRIC_1:def_12;
then A2: 0 <= real_dist . (x1,y1) by COMPLEX1:46;
 real_dist . (x2,y2) = abs (x2 - y2) by METRIC_1:def_12;
then A3: 0 <= real_dist . (x2,y2) by COMPLEX1:46;
assume  taxi_dist2 . (x,y) = 0 ; ::_thesis: x = y
then A4: (real_dist . (x1,y1)) + (real_dist . (x2,y2)) = 0 by A1, Def16;
then  real_dist . (x1,y1) = 0 by A2, A3, XREAL_1:27;
then A5: x1 = y1 by METRIC_1:8;
 real_dist . (x2,y2) = 0 by A4, A2, A3, XREAL_1:27;
hence  x = y by A1, A5, METRIC_1:8; ::_thesis: verum
end;
assume A6: x = y ; ::_thesis: taxi_dist2 . (x,y) = 0
then A7: real_dist . (x2,y2) = 0 by METRIC_1:8;
taxi_dist2 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) by A1, Def16
.= 0 by A6, A7, METRIC_1:8 ;
hence  taxi_dist2 . (x,y) = 0 ; ::_thesis: verum
end;

theorem Th20: :: METRIC_3:20
for x, y being Element of [:REAL,REAL:] holds taxi_dist2 . (x,y) = taxi_dist2 . (y,x)
proof
let x, y be Element of [:REAL,REAL:]; ::_thesis: taxi_dist2 . (x,y) = taxi_dist2 . (y,x)
reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 as Element of REAL ;
A1: ( x = [x1,x2] & y = [y1,y2] ) by MCART_1:22;
then taxi_dist2 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) by Def16
.= (real_dist . (y1,x1)) + (real_dist . (x2,y2)) by METRIC_1:9
.= (real_dist . (y1,x1)) + (real_dist . (y2,x2)) by METRIC_1:9
.= taxi_dist2 . (y,x) by A1, Def16 ;
hence  taxi_dist2 . (x,y) = taxi_dist2 . (y,x) ; ::_thesis: verum
end;

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))
proof
let x, y, z be Element of [:REAL,REAL:]; ::_thesis: taxi_dist2 . (x,z) <= (taxi_dist2 . (x,y)) + (taxi_dist2 . (y,z))
reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 , z1 = z `1 , z2 = z `2 as Element of REAL ;
A1: y = [y1,y2] by MCART_1:22;
set d5 = real_dist . (x2,y2);
set d6 = real_dist . (y2,z2);
set d3 = real_dist . (y1,z1);
set d4 = real_dist . (x2,z2);
set d1 = real_dist . (x1,z1);
set d2 = real_dist . (x1,y1);
A2: z = [z1,z2] by MCART_1:22;
A3: x = [x1,x2] by MCART_1:22;
then A4: taxi_dist2 . (x,z) = (real_dist . (x1,z1)) + (real_dist . (x2,z2)) by A2, Def16;
A5: ( real_dist . (x1,z1) <= (real_dist . (x1,y1)) + (real_dist . (y1,z1)) & real_dist . (x2,z2) <= (real_dist . (x2,y2)) + (real_dist . (y2,z2)) ) by METRIC_1:10;
((real_dist . (x1,y1)) + (real_dist . (y1,z1))) + ((real_dist . (x2,y2)) + (real_dist . (y2,z2))) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + ((real_dist . (y1,z1)) + (real_dist . (y2,z2)))
.= (taxi_dist2 . (x,y)) + ((real_dist . (y1,z1)) + (real_dist . (y2,z2))) by A3, A1, Def16
.= (taxi_dist2 . (x,y)) + (taxi_dist2 . (y,z)) by A1, A2, Def16 ;
hence  taxi_dist2 . (x,z) <= (taxi_dist2 . (x,y)) + (taxi_dist2 . (y,z)) by A5, A4, XREAL_1:7; ::_thesis: verum
end;

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
proof
now__::_thesis:_for_x,_y,_z_being_Element_of_MetrStruct(#_[:REAL,REAL:],taxi_dist2_#)_holds_
(_(_dist_(x,y)_=_0_implies_x_=_y_)_&_(_x_=_y_implies_dist_(x,y)_=_0_)_&_dist_(x,y)_=_dist_(y,x)_&_dist_(x,z)_<=_(dist_(x,y))_+_(dist_(y,z))_)
let x, y, z be Element of MetrStruct(# [:REAL,REAL:],taxi_dist2 #); ::_thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
reconsider x9 = x, y9 = y, z9 = z as Element of [:REAL,REAL:] ;
A1: dist (x,y) = taxi_dist2 . (x9,y9) by METRIC_1:def_1;
hence  ( dist (x,y) = 0 iff x = y ) by Th19; ::_thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
 dist (y,x) = taxi_dist2 . (y9,x9) by METRIC_1:def_1;
hence  dist (x,y) = dist (y,x) by A1, Th20; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
 ( dist (x,z) = taxi_dist2 . (x9,z9) & dist (y,z) = taxi_dist2 . (y9,z9) ) by METRIC_1:def_1;
hence  dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th21; ::_thesis: verum
end;
hence  MetrStruct(# [:REAL,REAL:],taxi_dist2 #) is non empty strict MetrSpace by METRIC_1:6; ::_thesis: verum
end;
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] & 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] & y = [y1,y2] holds
b1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))
proof
deffunc H1( Element of REAL , Element of REAL , Element of REAL , Element of REAL ) ->  Element of REAL = sqrt (((real_dist . ($1,$2)) ^2) + ((real_dist . ($3,$4)) ^2));
consider F being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL such that
A1: for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
F . (x,y) = H1(x1,y1,x2,y2) from METRIC_3:sch_1();
take  F ; ::_thesis: for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
F . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))
let x1, y1, x2, y2 be Element of REAL ; ::_thesis: for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
F . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))
let x, y be Element of [:REAL,REAL:]; ::_thesis: ( x = [x1,x2] & y = [y1,y2] implies F . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) )
assume  ( x = [x1,x2] & y = [y1,y2] ) ; ::_thesis: F . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))
hence  F . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) by A1; ::_thesis: verum
end;
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] & y = [y1,y2] holds
b1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ) & ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
b2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ) holds
b1 = b2
proof
let f1, f2 be Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL; ::_thesis: ( ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
f1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ) & ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
f2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ) implies f1 = f2 )
assume that
A2: for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
f1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) and
A3: for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
f2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ; ::_thesis: f1 = f2
 for x, y being Element of [:REAL,REAL:] holds f1 . (x,y) = f2 . (x,y)
proof
let x, y be Element of [:REAL,REAL:]; ::_thesis: f1 . (x,y) = f2 . (x,y)
consider x1, x2 being Element of REAL  such that
A4: x = [x1,x2] by DOMAIN_1:1;
consider y1, y2 being Element of REAL  such that
A5: y = [y1,y2] by DOMAIN_1:1;
thus f1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) by A2, A4, A5
.= f2 . (x,y) by A3, A4, A5 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
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] & 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 )
proof
let x, y be Element of [:REAL,REAL:]; ::_thesis: ( Eukl_dist2 . (x,y) = 0 iff x = y )
reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 as Element of REAL ;
A1: ( x = [x1,x2] & y = [y1,y2] ) by MCART_1:22;
thus  ( Eukl_dist2 . (x,y) = 0 implies x = y ) ::_thesis: ( x = y implies Eukl_dist2 . (x,y) = 0 )
proof
set d2 = real_dist . (x2,y2);
set d1 = real_dist . (x1,y1);
assume  Eukl_dist2 . (x,y) = 0 ; ::_thesis: x = y
then A2: sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) = 0 by A1, Def18;
A3: ( 0 <= (real_dist . (x1,y1)) ^2 & 0 <= (real_dist . (x2,y2)) ^2 ) by XREAL_1:63;
then  real_dist . (x1,y1) = 0 by A2, Lm1;
then A4: x1 = y1 by METRIC_1:8;
 real_dist . (x2,y2) = 0 by A2, A3, Lm1;
hence  x = y by A1, A4, METRIC_1:8; ::_thesis: verum
end;
assume  x = y ; ::_thesis: Eukl_dist2 . (x,y) = 0
then A5: ( (real_dist . (x1,y1)) ^2 = 0 ^2 & (real_dist . (x2,y2)) ^2 = 0 ^2 ) by METRIC_1:8;
Eukl_dist2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) by A1, Def18
.= 0 by A5, Lm1 ;
hence  Eukl_dist2 . (x,y) = 0 ; ::_thesis: verum
end;

theorem Th23: :: METRIC_3:23
for x, y being Element of [:REAL,REAL:] holds Eukl_dist2 . (x,y) = Eukl_dist2 . (y,x)
proof
let x, y be Element of [:REAL,REAL:]; ::_thesis: Eukl_dist2 . (x,y) = Eukl_dist2 . (y,x)
reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 as Element of REAL ;
A1: ( x = [x1,x2] & y = [y1,y2] ) by MCART_1:22;
then Eukl_dist2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) by Def18
.= sqrt (((real_dist . (y1,x1)) ^2) + ((real_dist . (x2,y2)) ^2)) by METRIC_1:9
.= sqrt (((real_dist . (y1,x1)) ^2) + ((real_dist . (y2,x2)) ^2)) by METRIC_1:9
.= Eukl_dist2 . (y,x) by A1, Def18 ;
hence  Eukl_dist2 . (x,y) = Eukl_dist2 . (y,x) ; ::_thesis: verum
end;

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))
proof
let x, y, z be Element of [:REAL,REAL:]; ::_thesis: Eukl_dist2 . (x,z) <= (Eukl_dist2 . (x,y)) + (Eukl_dist2 . (y,z))
reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 , z1 = z `1 , z2 = z `2 as Element of REAL ;
A1: x = [x1,x2] by MCART_1:22;
set d5 = real_dist . (x2,y2);
set d3 = real_dist . (y1,z1);
set d1 = real_dist . (x1,z1);
A2: y = [y1,y2] by MCART_1:22;
set d6 = real_dist . (y2,z2);
set d4 = real_dist . (x2,z2);
set d2 = real_dist . (x1,y1);
A3: z = [z1,z2] by MCART_1:22;
 real_dist . (x2,z2) = abs (x2 - z2) by METRIC_1:def_12;
then  0 <= real_dist . (x2,z2) by COMPLEX1:46;
then A4: (real_dist . (x2,z2)) ^2 <= ((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2 by METRIC_1:10, SQUARE_1:15;
 ( 0 <= (real_dist . (x1,z1)) ^2 & 0 <= (real_dist . (x2,z2)) ^2 ) by XREAL_1:63;
then A5: 0 + 0 <= ((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2) by XREAL_1:7;
 real_dist . (x1,z1) = abs (x1 - z1) by METRIC_1:def_12;
then  0 <= real_dist . (x1,z1) by COMPLEX1:46;
then  (real_dist . (x1,z1)) ^2 <= ((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2 by METRIC_1:10, SQUARE_1:15;
then  ((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2) <= (((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2) + (((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2) by A4, XREAL_1:7;
then A6: sqrt (((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2)) <= sqrt ((((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2) + (((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2)) by A5, SQUARE_1:26;
 real_dist . (y2,z2) = abs (y2 - z2) by METRIC_1:def_12;
then A7: 0 <= real_dist . (y2,z2) by COMPLEX1:46;
 real_dist . (x2,y2) = abs (x2 - y2) by METRIC_1:def_12;
then A8: 0 <= real_dist . (x2,y2) by COMPLEX1:46;
 real_dist . (y1,z1) = abs (y1 - z1) by METRIC_1:def_12;
then A9: 0 <= real_dist . (y1,z1) by COMPLEX1:46;
 real_dist . (x1,y1) = abs (x1 - y1) by METRIC_1:def_12;
then  0 <= real_dist . (x1,y1) by COMPLEX1:46;
then  sqrt ((((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2) + (((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2)) <= (sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))) + (sqrt (((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2))) by A9, A8, A7, Th12;
then  sqrt (((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2)) <= (sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))) + (sqrt (((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2))) by A6, XXREAL_0:2;
then  Eukl_dist2 . (x,z) <= (sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))) + (sqrt (((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2))) by A1, A3, Def18;
then  Eukl_dist2 . (x,z) <= (Eukl_dist2 . (x,y)) + (sqrt (((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2))) by A1, A2, Def18;
hence  Eukl_dist2 . (x,z) <= (Eukl_dist2 . (x,y)) + (Eukl_dist2 . (y,z)) by A2, A3, Def18; ::_thesis: verum
end;

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
proof
now__::_thesis:_for_x,_y,_z_being_Element_of_MetrStruct(#_[:REAL,REAL:],Eukl_dist2_#)_holds_
(_(_dist_(x,y)_=_0_implies_x_=_y_)_&_(_x_=_y_implies_dist_(x,y)_=_0_)_&_dist_(x,y)_=_dist_(y,x)_&_dist_(x,z)_<=_(dist_(x,y))_+_(dist_(y,z))_)
let x, y, z be Element of MetrStruct(# [:REAL,REAL:],Eukl_dist2 #); ::_thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
reconsider x9 = x, y9 = y, z9 = z as Element of [:REAL,REAL:] ;
A1: dist (x,y) = Eukl_dist2 . (x9,y9) by METRIC_1:def_1;
hence  ( dist (x,y) = 0 iff x = y ) by Th22; ::_thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
 dist (y,x) = Eukl_dist2 . (y9,x9) by METRIC_1:def_1;
hence  dist (x,y) = dist (y,x) by A1, Th23; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
 ( dist (x,z) = Eukl_dist2 . (x9,z9) & dist (y,z) = Eukl_dist2 . (y9,z9) ) by METRIC_1:def_1;
hence  dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th24; ::_thesis: verum
end;
hence  MetrStruct(# [:REAL,REAL:],Eukl_dist2 #) is non empty strict MetrSpace by METRIC_1:6; ::_thesis: verum
end;
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] & 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] & y = [y1,y2,y3] holds
b1 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3))
proof
deffunc H1( Element of REAL , Element of REAL , Element of REAL , Element of REAL , Element of REAL , Element of REAL ) ->  Element of REAL = ((real_dist . ($1,$2)) + (real_dist . ($3,$4))) + (real_dist . ($5,$6));
consider F being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL such that
A1: 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] & y = [y1,y2,y3] holds
F . (x,y) = H1(x1,y1,x2,y2,x3,y3) from METRIC_3:sch_2();
take  F ; ::_thesis: 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] & y = [y1,y2,y3] holds
F . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3))
let x1, y1, x2, y2, x3, y3 be Element of REAL ; ::_thesis: for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
F . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3))
let x, y be Element of [:REAL,REAL,REAL:]; ::_thesis: ( x = [x1,x2,x3] & y = [y1,y2,y3] implies F . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) )
assume  ( x = [x1,x2,x3] & y = [y1,y2,y3] ) ; ::_thesis: F . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3))
hence  F . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) by A1; ::_thesis: verum
end;
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] & y = [y1,y2,y3] holds
b1 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) ) & ( 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] & y = [y1,y2,y3] holds
b2 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) ) holds
b1 = b2
proof
let f1, f2 be Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL; ::_thesis: ( ( 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] & y = [y1,y2,y3] holds
f1 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) ) & ( 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] & y = [y1,y2,y3] holds
f2 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) ) implies f1 = f2 )
assume that
A2: 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] & y = [y1,y2,y3] holds
f1 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) and
A3: 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] & y = [y1,y2,y3] holds
f2 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) ; ::_thesis: f1 = f2
 for x, y being Element of [:REAL,REAL,REAL:] holds f1 . (x,y) = f2 . (x,y)
proof
let x, y be Element of [:REAL,REAL,REAL:]; ::_thesis: f1 . (x,y) = f2 . (x,y)
consider x1, x2, x3 being Element of REAL  such that
A4: x = [x1,x2,x3] by DOMAIN_1:3;
consider y1, y2, y3 being Element of REAL  such that
A5: y = [y1,y2,y3] by DOMAIN_1:3;
thus f1 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) by A2, A4, A5
.= f2 . (x,y) by A3, A4, A5 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
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] & 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 )
proof
let x, y be Element of [:REAL,REAL,REAL:]; ::_thesis: ( taxi_dist3 . (x,y) = 0 iff x = y )
reconsider x1 = x `1_3 , x2 = x `2_3 , x3 = x `3_3 , y1 = y `1_3 , y2 = y `2_3 , y3 = y `3_3 as Element of REAL ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) by MCART_1:44;
thus  ( taxi_dist3 . (x,y) = 0 implies x = y ) ::_thesis: ( x = y implies taxi_dist3 . (x,y) = 0 )
proof
set d3 = real_dist . (x3,y3);
set d2 = real_dist . (x2,y2);
set d1 = real_dist . (x1,y1);
set d4 = (real_dist . (x1,y1)) + (real_dist . (x2,y2));
 real_dist . (x3,y3) = abs (x3 - y3) by METRIC_1:def_12;
then A2: 0 <= real_dist . (x3,y3) by COMPLEX1:46;
 real_dist . (x1,y1) = abs (x1 - y1) by METRIC_1:def_12;
then A3: 0 <= real_dist . (x1,y1) by COMPLEX1:46;
assume  taxi_dist3 . (x,y) = 0 ; ::_thesis: x = y
then A4: ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) = 0 by A1, Def20;
 real_dist . (x2,y2) = abs (x2 - y2) by METRIC_1:def_12;
then A5: 0 <= real_dist . (x2,y2) by COMPLEX1:46;
then A6: 0 + 0 <= (real_dist . (x1,y1)) + (real_dist . (x2,y2)) by A3, XREAL_1:7;
then A7: (real_dist . (x1,y1)) + (real_dist . (x2,y2)) = 0 by A4, A2, XREAL_1:27;
then  real_dist . (x1,y1) = 0 by A5, A3, XREAL_1:27;
then A8: x1 = y1 by METRIC_1:8;
 real_dist . (x3,y3) = 0 by A4, A2, A6, XREAL_1:27;
then A9: x3 = y3 by METRIC_1:8;
 real_dist . (x2,y2) = 0 by A5, A3, A7, XREAL_1:27;
hence  x = y by A1, A9, A8, METRIC_1:8; ::_thesis: verum
end;
assume A10: x = y ; ::_thesis: taxi_dist3 . (x,y) = 0
then A11: ( real_dist . (x1,y1) = 0 & real_dist . (x2,y2) = 0 ) by METRIC_1:8;
taxi_dist3 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) by A1, Def20
.= 0 by A10, A11, METRIC_1:8 ;
hence  taxi_dist3 . (x,y) = 0 ; ::_thesis: verum
end;

theorem Th26: :: METRIC_3:26
for x, y being Element of [:REAL,REAL,REAL:] holds taxi_dist3 . (x,y) = taxi_dist3 . (y,x)
proof
let x, y be Element of [:REAL,REAL,REAL:]; ::_thesis: taxi_dist3 . (x,y) = taxi_dist3 . (y,x)
reconsider x1 = x `1_3 , x2 = x `2_3 , x3 = x `3_3 , y1 = y `1_3 , y2 = y `2_3 , y3 = y `3_3 as Element of REAL ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) by MCART_1:44;
then taxi_dist3 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) by Def20
.= ((real_dist . (y1,x1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) by METRIC_1:9
.= ((real_dist . (y1,x1)) + (real_dist . (y2,x2))) + (real_dist . (x3,y3)) by METRIC_1:9
.= ((real_dist . (y1,x1)) + (real_dist . (y2,x2))) + (real_dist . (y3,x3)) by METRIC_1:9
.= taxi_dist3 . (y,x) by A1, Def20 ;
hence  taxi_dist3 . (x,y) = taxi_dist3 . (y,x) ; ::_thesis: verum
end;

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))
proof
let x, y, z be Element of [:REAL,REAL,REAL:]; ::_thesis: taxi_dist3 . (x,z) <= (taxi_dist3 . (x,y)) + (taxi_dist3 . (y,z))
reconsider x1 = x `1_3 , x2 = x `2_3 , x3 = x `3_3 , y1 = y `1_3 , y2 = y `2_3 , y3 = y `3_3 , z1 = z `1_3 , z2 = z `2_3 , z3 = z `3_3 as Element of REAL ;
A1: x = [x1,x2,x3] by MCART_1:44;
set d7 = real_dist . (x3,z3);
set d8 = real_dist . (x3,y3);
set d3 = real_dist . (y1,z1);
set d4 = real_dist . (x2,z2);
A2: z = [z1,z2,z3] by MCART_1:44;
set d9 = real_dist . (y3,z3);
set d5 = real_dist . (x2,y2);
set d6 = real_dist . (y2,z2);
set d1 = real_dist . (x1,z1);
set d2 = real_dist . (x1,y1);
A3: y = [y1,y2,y3] by MCART_1:44;
set d10 = (real_dist . (x1,z1)) + (real_dist . (x2,z2));
 ( real_dist . (x1,z1) <= (real_dist . (x1,y1)) + (real_dist . (y1,z1)) & real_dist . (x2,z2) <= (real_dist . (x2,y2)) + (real_dist . (y2,z2)) ) by METRIC_1:10;
then A4: (real_dist . (x1,z1)) + (real_dist . (x2,z2)) <= ((real_dist . (x1,y1)) + (real_dist . (y1,z1))) + ((real_dist . (x2,y2)) + (real_dist . (y2,z2))) by XREAL_1:7;
 real_dist . (x3,z3) <= (real_dist . (x3,y3)) + (real_dist . (y3,z3)) by METRIC_1:10;
then A5: ((real_dist . (x1,z1)) + (real_dist . (x2,z2))) + (real_dist . (x3,z3)) <= (((real_dist . (x1,y1)) + (real_dist . (y1,z1))) + ((real_dist . (x2,y2)) + (real_dist . (y2,z2)))) + ((real_dist . (x3,y3)) + (real_dist . (y3,z3))) by A4, XREAL_1:7;
(((real_dist . (x1,y1)) + (real_dist . (y1,z1))) + ((real_dist . (x2,y2)) + (real_dist . (y2,z2)))) + ((real_dist . (x3,y3)) + (real_dist . (y3,z3))) = (((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3))) + (((real_dist . (y1,z1)) + (real_dist . (y2,z2))) + (real_dist . (y3,z3)))
.= (taxi_dist3 . (x,y)) + (((real_dist . (y1,z1)) + (real_dist . (y2,z2))) + (real_dist . (y3,z3))) by A1, A3, Def20
.= (taxi_dist3 . (x,y)) + (taxi_dist3 . (y,z)) by A3, A2, Def20 ;
hence  taxi_dist3 . (x,z) <= (taxi_dist3 . (x,y)) + (taxi_dist3 . (y,z)) by A1, A2, A5, Def20; ::_thesis: verum
end;

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
proof
now__::_thesis:_for_x,_y,_z_being_Element_of_MetrStruct(#_[:REAL,REAL,REAL:],taxi_dist3_#)_holds_
(_(_dist_(x,y)_=_0_implies_x_=_y_)_&_(_x_=_y_implies_dist_(x,y)_=_0_)_&_dist_(x,y)_=_dist_(y,x)_&_dist_(x,z)_<=_(dist_(x,y))_+_(dist_(y,z))_)
let x, y, z be Element of MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #); ::_thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
reconsider x9 = x, y9 = y, z9 = z as Element of [:REAL,REAL,REAL:] ;
A1: dist (x,y) = taxi_dist3 . (x9,y9) by METRIC_1:def_1;
hence  ( dist (x,y) = 0 iff x = y ) by Th25; ::_thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
 dist (y,x) = taxi_dist3 . (y9,x9) by METRIC_1:def_1;
hence  dist (x,y) = dist (y,x) by A1, Th26; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
 ( dist (x,z) = taxi_dist3 . (x9,z9) & dist (y,z) = taxi_dist3 . (y9,z9) ) by METRIC_1:def_1;
hence  dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th27; ::_thesis: verum
end;
hence  MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #) is non empty strict MetrSpace by METRIC_1:6; ::_thesis: verum
end;
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] & 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] & y = [y1,y2,y3] holds
b1 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))
proof
deffunc H1( Element of REAL , Element of REAL , Element of REAL , Element of REAL , Element of REAL , Element of REAL ) ->  Element of REAL = sqrt ((((real_dist . ($1,$2)) ^2) + ((real_dist . ($3,$4)) ^2)) + ((real_dist . ($5,$6)) ^2));
consider F being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL such that
A1: 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] & y = [y1,y2,y3] holds
F . (x,y) = H1(x1,y1,x2,y2,x3,y3) from METRIC_3:sch_2();
take  F ; ::_thesis: 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] & y = [y1,y2,y3] holds
F . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))
let x1, y1, x2, y2, x3, y3 be Element of REAL ; ::_thesis: for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
F . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))
let x, y be Element of [:REAL,REAL,REAL:]; ::_thesis: ( x = [x1,x2,x3] & y = [y1,y2,y3] implies F . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) )
assume  ( x = [x1,x2,x3] & y = [y1,y2,y3] ) ; ::_thesis: F . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))
hence  F . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) by A1; ::_thesis: verum
end;
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] & y = [y1,y2,y3] holds
b1 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) ) & ( 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] & 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
proof
let f1, f2 be Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL; ::_thesis: ( ( 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] & y = [y1,y2,y3] holds
f1 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) ) & ( 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] & y = [y1,y2,y3] holds
f2 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) ) implies f1 = f2 )
assume that
A2: 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] & y = [y1,y2,y3] holds
f1 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) and
A3: 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] & y = [y1,y2,y3] holds
f2 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) ; ::_thesis: f1 = f2
 for x, y being Element of [:REAL,REAL,REAL:] holds f1 . (x,y) = f2 . (x,y)
proof
let x, y be Element of [:REAL,REAL,REAL:]; ::_thesis: f1 . (x,y) = f2 . (x,y)
consider x1, x2, x3 being Element of REAL  such that
A4: x = [x1,x2,x3] by DOMAIN_1:3;
consider y1, y2, y3 being Element of REAL  such that
A5: y = [y1,y2,y3] by DOMAIN_1:3;
thus f1 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) by A2, A4, A5
.= f2 . (x,y) by A3, A4, A5 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
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] & 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 )
proof
let x, y be Element of [:REAL,REAL,REAL:]; ::_thesis: ( Eukl_dist3 . (x,y) = 0 iff x = y )
reconsider x1 = x `1_3 , x2 = x `2_3 , x3 = x `3_3 , y1 = y `1_3 , y2 = y `2_3 , y3 = y `3_3 as Element of REAL ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) by MCART_1:44;
thus  ( Eukl_dist3 . (x,y) = 0 implies x = y ) ::_thesis: ( x = y implies Eukl_dist3 . (x,y) = 0 )
proof
set d3 = real_dist . (x3,y3);
set d2 = real_dist . (x2,y2);
set d1 = real_dist . (x1,y1);
A2: ( 0 <= (real_dist . (x2,y2)) ^2 & 0 <= (real_dist . (x3,y3)) ^2 ) by XREAL_1:63;
assume  Eukl_dist3 . (x,y) = 0 ; ::_thesis: x = y
then  sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) = 0 by A1, Def22;
then A3: sqrt (((real_dist . (x1,y1)) ^2) + (((real_dist . (x2,y2)) ^2) + ((real_dist . (x3,y3)) ^2))) = 0 ;
 ( 0 <= (real_dist . (x2,y2)) ^2 & 0 <= (real_dist . (x3,y3)) ^2 ) by XREAL_1:63;
then A4: ( 0 <= (real_dist . (x1,y1)) ^2 & 0 + 0 <= ((real_dist . (x2,y2)) ^2) + ((real_dist . (x3,y3)) ^2) ) by XREAL_1:7, XREAL_1:63;
then  real_dist . (x1,y1) = 0 by A3, Lm1;
then A5: x1 = y1 by METRIC_1:8;
A6: ((real_dist . (x2,y2)) ^2) + ((real_dist . (x3,y3)) ^2) = 0 by A3, A4, Lm1;
then  real_dist . (x2,y2) = 0 by A2, XREAL_1:27;
then A7: x2 = y2 by METRIC_1:8;
 real_dist . (x3,y3) = 0 by A6, A2, XREAL_1:27;
hence  x = y by A1, A5, A7, METRIC_1:8; ::_thesis: verum
end;
assume A8: x = y ; ::_thesis: Eukl_dist3 . (x,y) = 0
then A9: ( (real_dist . (x1,y1)) ^2 = 0 ^2 & (real_dist . (x2,y2)) ^2 = 0 ^2 ) by METRIC_1:8;
Eukl_dist3 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) by A1, Def22
.= 0 ^2 by A8, A9, METRIC_1:8, SQUARE_1:17 ;
hence  Eukl_dist3 . (x,y) = 0 ; ::_thesis: verum
end;

theorem Th29: :: METRIC_3:29
for x, y being Element of [:REAL,REAL,REAL:] holds Eukl_dist3 . (x,y) = Eukl_dist3 . (y,x)
proof
let x, y be Element of [:REAL,REAL,REAL:]; ::_thesis: Eukl_dist3 . (x,y) = Eukl_dist3 . (y,x)
reconsider x1 = x `1_3 , x2 = x `2_3 , x3 = x `3_3 , y1 = y `1_3 , y2 = y `2_3 , y3 = y `3_3 as Element of REAL ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) by MCART_1:44;
then Eukl_dist3 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) by Def22
.= sqrt ((((real_dist . (y1,x1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) by METRIC_1:9
.= sqrt ((((real_dist . (y1,x1)) ^2) + ((real_dist . (y2,x2)) ^2)) + ((real_dist . (x3,y3)) ^2)) by METRIC_1:9
.= sqrt ((((real_dist . (y1,x1)) ^2) + ((real_dist . (y2,x2)) ^2)) + ((real_dist . (y3,x3)) ^2)) by METRIC_1:9
.= Eukl_dist3 . (y,x) by A1, Def22 ;
hence  Eukl_dist3 . (x,y) = Eukl_dist3 . (y,x) ; ::_thesis: verum
end;

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))
proof
let x, y, z be Element of [:REAL,REAL,REAL:]; ::_thesis: Eukl_dist3 . (x,z) <= (Eukl_dist3 . (x,y)) + (Eukl_dist3 . (y,z))
reconsider x1 = x `1_3 , x2 = x `2_3 , x3 = x `3_3 , y1 = y `1_3 , y2 = y `2_3 , y3 = y `3_3 , z1 = z `1_3 , z2 = z `2_3 , z3 = z `3_3 as Element of REAL ;
A1: x = [x1,x2,x3] by MCART_1:44;
set d9 = real_dist . (y3,z3);
set d5 = real_dist . (x2,y2);
set d6 = real_dist . (y2,z2);
set d1 = real_dist . (x1,z1);
set d2 = real_dist . (x1,y1);
A2: y = [y1,y2,y3] by MCART_1:44;
 real_dist . (y3,z3) = abs (y3 - z3) by METRIC_1:def_12;
then A3: 0 <= real_dist . (y3,z3) by COMPLEX1:46;
 real_dist . (y2,z2) = abs (y2 - z2) by METRIC_1:def_12;
then A4: 0 <= real_dist . (y2,z2) by COMPLEX1:46;
 real_dist . (x2,y2) = abs (x2 - y2) by METRIC_1:def_12;
then A5: 0 <= real_dist . (x2,y2) by COMPLEX1:46;
set d7 = real_dist . (x3,z3);
set d8 = real_dist . (x3,y3);
set d3 = real_dist . (y1,z1);
set d4 = real_dist . (x2,z2);
A6: z = [z1,z2,z3] by MCART_1:44;
 real_dist . (x3,z3) = abs (x3 - z3) by METRIC_1:def_12;
then  0 <= real_dist . (x3,z3) by COMPLEX1:46;
then A7: (real_dist . (x3,z3)) ^2 <= ((real_dist . (x3,y3)) + (real_dist . (y3,z3))) ^2 by METRIC_1:10, SQUARE_1:15;
 real_dist . (x2,z2) = abs (x2 - z2) by METRIC_1:def_12;
then  0 <= real_dist . (x2,z2) by COMPLEX1:46;
then A8: (real_dist . (x2,z2)) ^2 <= ((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2 by METRIC_1:10, SQUARE_1:15;
 real_dist . (x1,z1) = abs (x1 - z1) by METRIC_1:def_12;
then  0 <= real_dist . (x1,z1) by COMPLEX1:46;
then  (real_dist . (x1,z1)) ^2 <= ((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2 by METRIC_1:10, SQUARE_1:15;
then  ((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2) <= (((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2) + (((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2) by A8, XREAL_1:7;
then A9: (((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2)) + ((real_dist . (x3,z3)) ^2) <= ((((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2) + (((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2)) + (((real_dist . (x3,y3)) + (real_dist . (y3,z3))) ^2) by A7, XREAL_1:7;
 ( 0 <= (real_dist . (x1,z1)) ^2 & 0 <= (real_dist . (x2,z2)) ^2 ) by XREAL_1:63;
then A10: 0 + 0 <= ((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2) by XREAL_1:7;
 0 <= (real_dist . (x3,z3)) ^2 by XREAL_1:63;
then  0 + 0 <= (((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2)) + ((real_dist . (x3,z3)) ^2) by A10, XREAL_1:7;
then A11: sqrt ((((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2)) + ((real_dist . (x3,z3)) ^2)) <= sqrt (((((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2) + (((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2)) + (((real_dist . (x3,y3)) + (real_dist . (y3,z3))) ^2)) by A9, SQUARE_1:26;
 real_dist . (x3,y3) = abs (x3 - y3) by METRIC_1:def_12;
then A12: 0 <= real_dist . (x3,y3) by COMPLEX1:46;
 real_dist . (y1,z1) = abs (y1 - z1) by METRIC_1:def_12;
then A13: 0 <= real_dist . (y1,z1) by COMPLEX1:46;
 real_dist . (x1,y1) = abs (x1 - y1) by METRIC_1:def_12;
then  0 <= real_dist . (x1,y1) by COMPLEX1:46;
then  sqrt (((((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2) + (((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2)) + (((real_dist . (x3,y3)) + (real_dist . (y3,z3))) ^2)) <= (sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))) + (sqrt ((((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2)) + ((real_dist . (y3,z3)) ^2))) by A13, A5, A4, A12, A3, Lm2;
then  sqrt ((((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2)) + ((real_dist . (x3,z3)) ^2)) <= (sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))) + (sqrt ((((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2)) + ((real_dist . (y3,z3)) ^2))) by A11, XXREAL_0:2;
then  Eukl_dist3 . (x,z) <= (sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))) + (sqrt ((((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2)) + ((real_dist . (y3,z3)) ^2))) by A1, A6, Def22;
then  Eukl_dist3 . (x,z) <= (Eukl_dist3 . (x,y)) + (sqrt ((((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2)) + ((real_dist . (y3,z3)) ^2))) by A1, A2, Def22;
hence  Eukl_dist3 . (x,z) <= (Eukl_dist3 . (x,y)) + (Eukl_dist3 . (y,z)) by A2, A6, Def22; ::_thesis: verum
end;

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
proof
now__::_thesis:_for_x,_y,_z_being_Element_of_MetrStruct(#_[:REAL,REAL,REAL:],Eukl_dist3_#)_holds_
(_(_dist_(x,y)_=_0_implies_x_=_y_)_&_(_x_=_y_implies_dist_(x,y)_=_0_)_&_dist_(x,y)_=_dist_(y,x)_&_dist_(x,z)_<=_(dist_(x,y))_+_(dist_(y,z))_)
let x, y, z be Element of MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #); ::_thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
reconsider x9 = x, y9 = y, z9 = z as Element of [:REAL,REAL,REAL:] ;
A1: dist (x,y) = Eukl_dist3 . (x9,y9) by METRIC_1:def_1;
hence  ( dist (x,y) = 0 iff x = y ) by Th28; ::_thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
 dist (y,x) = Eukl_dist3 . (y9,x9) by METRIC_1:def_1;
hence  dist (x,y) = dist (y,x) by A1, Th29; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
 ( dist (x,z) = Eukl_dist3 . (x9,z9) & dist (y,z) = Eukl_dist3 . (y9,z9) ) by METRIC_1:def_1;
hence  dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th30; ::_thesis: verum
end;
hence  MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #) is non empty strict MetrSpace by METRIC_1:6; ::_thesis: verum
end;
end;

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