:: 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 #);