The Mizar article:

Metrics in the Cartesian Product --- Part II

by
Stanislawa Kanas, and
Adam Lecko

Received July 8, 1991

Copyright (c) 1991 Association of Mizar Users

MML identifier: METRIC_4
[ MML identifier index ]


environ

 vocabulary METRIC_1, FUNCT_1, SQUARE_1, ARYTM_1, ABSVALUE, METRIC_4;
 notation ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, REAL_1, FUNCT_2, ABSVALUE,
      STRUCT_0, METRIC_1, DOMAIN_1, SQUARE_1;
 constructors REAL_1, ABSVALUE, METRIC_1, DOMAIN_1, SQUARE_1, MEMBERED,
      XBOOLE_0;
 clusters SUBSET_1, METRIC_1, METRIC_3, STRUCT_0, RELSET_1, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 theorems BINOP_1, DOMAIN_1, ZFMISC_1, METRIC_1, METRIC_3, REAL_1, MCART_1,
      AXIOMS, SQUARE_1, ABSVALUE, XCMPLX_0, XCMPLX_1;
 schemes METRIC_3;

begin :: METRICS IN THE CARTESIAN PRODUCT OF TWO SETS

reserve X,Y for non empty MetrSpace;
reserve x1,y1,z1 for Element of X;
reserve x2,y2,z2 for Element of Y;

definition let X,Y;
  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
  :Def1: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
    proof
     deffunc G(Element of X,Element of X,
               Element of Y,Element of Y) =
               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] = G(x1,y1,x2,y2) from LambdaMCART;
        take F;
      let x1,y1 be Element of X,
          x2,y2 be Element of Y,
          x,y be Element of [:the carrier of X,the carrier of Y:] such that
          A2: ( x = [x1,x2] & y = [y1,y2] );
      thus F.(x,y) = F.[x,y] by BINOP_1:def 1
                  .= sqrt((dist(x1,y1))^2 + (dist(x2,y2)^2)) by A1,A2;
     end;
   uniqueness
    proof
    let f1,f2 be Function of [:[:the carrier of X,the carrier of Y:],
                    [:the carrier of X,the carrier of Y:]:],REAL;

    assume that
    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
           f1.(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2)^2)) and
    A4: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);
      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:];
        consider x1 be Element of X,
                      x2 be Element of Y
        such that
        A5: x = [x1,x2] by DOMAIN_1:9;
        consider y1 be Element of X,
                      y2 be Element of Y
        such that
        A6: y = [y1,y2] by DOMAIN_1:9;
        thus f1.(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2)^2)) by A3,A5,A6
                     .= f2.(x,y) by A4,A5,A6;
       end;
   hence thesis by BINOP_1:2;
    end;
   end;

reserve a,b for Element of REAL;

canceled;

   theorem
    Th2:for a,b being Element of REAL
         st 0 <= a & 0 <= b holds
             sqrt(a + b) = 0 iff ( a = 0 & b = 0)
       proof
        let a,b such that A1: 0 <= a & 0 <= b;
         thus sqrt(a + b) = 0 implies (a = 0 & b = 0)
          proof
          assume
           A2:sqrt(a + b) = 0;
             0 + 0 <= a + b by A1,REAL_1:55;
           then a + b = 0 by A2,SQUARE_1:92;
           hence thesis by A1,METRIC_3:2;
          end;
         thus a = 0 & b = 0 implies sqrt(a + b) = 0 by SQUARE_1:82;
       end;

   theorem Th3:
    for x,y being Element of [:the carrier of X,the carrier of Y:]
            st (x = [x1,x2] & y = [y1,y2]) holds
    dist_cart2S(X,Y).(x,y) = 0 iff x = y
     proof
      let x,y be Element of [:the carrier of X,the carrier of Y:] such that
      A1:x = [x1,x2] & y = [y1,y2];
      thus dist_cart2S(X,Y).(x,y) = 0 implies x = y
       proof
        assume A2:dist_cart2S(X,Y).(x,y) = 0;
        set d1 = dist(x1,y1);
        set d2 = dist(x2,y2);
        A3:sqrt(d1^2 + d2^2) = 0 by A1,A2,Def1;
        A4: 0 <= d1^2 by SQUARE_1:72;
A5:        0 <= d2^2 by SQUARE_1:72;
        then A6:d1^2 = 0 & d2^2 = 0 by A3,A4,Th2;
          d1^2 = 0 by A3,A4,A5,Th2;
        then d1 = 0 by SQUARE_1:73;
        then A7: x1 = y1 by METRIC_1:2;
          d2 = 0 by A6,SQUARE_1:73;
        hence thesis by A1,A7,METRIC_1:2;
       end;
        assume x = y;
        then A8:x1 = y1 & x2 = y2 by A1,ZFMISC_1:33;
        then A9:(dist(x1,y1))^2 = 0 by METRIC_1:1,SQUARE_1:60;
        A10: (dist(x2,y2))^2 = 0 by A8,METRIC_1:1,SQUARE_1:60;
          dist_cart2S(X,Y).(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2)
                                                   by A1,Def1
                              .= 0 by A9,A10,Th2;
        hence thesis;
        end;

   theorem Th4:
    for x,y being Element of [:the carrier of X,the carrier of Y:]
            st (x = [x1,x2] & y = [y1,y2]) holds
    dist_cart2S(X,Y).(x,y) = dist_cart2S(X,Y).(y,x)
     proof
      let x,y be Element of [:the carrier of X,the carrier of Y:]; assume
      A1:x = [x1,x2] & y = [y1,y2];
      then dist_cart2S(X,Y).(x,y) = sqrt((dist(y1,x1))^2 + (dist(x2,y2))^2)
by Def1
                              .= dist_cart2S(X,Y).(y,x) by A1,Def1;
      hence thesis;
     end;

   theorem Th5:
    for a,b,c,d being Element of REAL
       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 Element of REAL such that
     A1: 0 <= a & 0 <= b & 0 <= c & 0 <= d;
       0 <= ((a*d) - (c*b))^2 by SQUARE_1:72;
     then 0 <= (a*d)^2 - 2*(a*d)*(c*b) + (c*b)^2 by SQUARE_1:64;
     then 0 <= a^2*d^2 - 2*(a*d)*(c*b) + (c*b)^2 by SQUARE_1:68;
     then 0 <= a^2*d^2 - 2*(a*d)*(c*b) + c^2*b^2 by SQUARE_1:68;
     then 0 <= a^2*d^2 + (- 2*(a*d)*(c*b)) + c^2*b^2 by XCMPLX_0:def 8;
     then 0 <= a^2*d^2 + c^2*b^2 + (- 2*(a*d)*(c*b)) by XCMPLX_1:1;
     then 0 <= (a^2*d^2 + c^2*b^2) - 2*(a*d)*(c*b) by XCMPLX_0:def 8;
     then 0 + 2*(a*d)*(c*b) <= (a^2*d^2 + c^2*b^2) by REAL_1:84;
     then (b^2*d^2) + 2*(a*d)*(c*b) <= (a^2*d^2 + c^2*b^2) + (b^2*d^2
) by AXIOMS:24;
     then (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 AXIOMS:24;
     then (a^2*c^2) + (2*(a*d)*(c*b) + (b^2*d^2)) <=
                      (a^2*c^2) + (a^2*d^2 + c^2*b^2) + (b^2*d^2) by XCMPLX_1:1
;
     then (a^2*c^2) + (2*(a*d)*(c*b) + b^2*d^2) <=
                      (a^2*c^2 + a^2*d^2) + c^2*b^2 + (b^2*d^2) by XCMPLX_1:1;
     then a^2*c^2 + (2*(a*d)*(c*b) + b^2*d^2) <=
                            (a^2*(c^2 + d^2)) + c^2*b^2 + d^2*b^2 by XCMPLX_1:8
;
     then a^2*c^2 + (2*(a*d)*(c*b) + b^2*d^2) <=
                            (a^2*(c^2 + d^2)) + (c^2*b^2 + d^2*b^2
) by XCMPLX_1:1;
     then a^2*c^2 + (2*(a*d)*(c*b) + b^2*d^2) <=
                            (a^2*(c^2 + d^2)) + (b^2*(c^2 + d^2)) by XCMPLX_1:8
;
     then a^2*c^2 + 2*(a*d)*(c*b) + b^2*d^2 <=
                            a^2*(c^2 + d^2) + (b^2*(c^2 + d^2)) by XCMPLX_1:1;
     then a^2*c^2 + 2*(a*d)*(c*b) + b^2*d^2 <=
                            (a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:8;
     then (a*c)^2 + 2*(a*d)*(c*b) + b^2*d^2 <=
                            (a^2 + b^2)*(c^2 + d^2) by SQUARE_1:68;
     then (a*c)^2 + 2*(a*d)*(c*b) + (b*d)^2 <=
                            (a^2 + b^2)*(c^2 + d^2) by SQUARE_1:68;
     then (a*c)^2 + 2*((a*d)*(c*b)) + (b*d)^2 <=
                            (a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:4;
     then (a*c)^2 + 2*(((a*d)*c)*b) + (b*d)^2 <=
                            (a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:4;
     then (a*c)^2 + 2*(((a*c)*d)*b) + (b*d)^2 <=
                            (a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:4;
     then (a*c)^2 + 2*((a*c)*(d*b)) + (b*d)^2 <=
                            (a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:4;
     then (a*c)^2 + 2*(a*c)*(d*b) + (d*b)^2 <=
                            (a^2 + b^2)*(c^2 + d^2) by XCMPLX_1:4;
     then A2: (a*c + d*b)^2 <= (a^2 + b^2)*(c^2 + d^2) by SQUARE_1:63;
       0 <= (a*c + d*b)^2 by SQUARE_1:72;
     then sqrt((a*c + d*b)^2) <= sqrt((a^2 + b^2)*(c^2 + d^2
)) by A2,SQUARE_1:94;
     then A3: 2*sqrt((a*c + d*b)^2) <= 2*(sqrt((a^2 + b^2)*(c^2 + d^2)))
                     by AXIOMS:25;
     A4: 0 <= a^2 by SQUARE_1:72;
       0 <= b^2 by SQUARE_1:72;
     then A5: 0 + 0 <= a^2 + b^2 by A4,REAL_1:55;
     A6: 0 <= d^2 by SQUARE_1:72;
       0 <= c^2 by SQUARE_1:72;
     then A7: 0 + 0 <= c^2 + d^2 by A6,REAL_1:55;
     then A8: 2*sqrt((a*c + d*b)^2) <= 2*(sqrt(a^2 + b^2)*sqrt(c^2 + d^2))
                     by A3,A5,SQUARE_1:97;
     A9: 0 <= a*c by A1,SQUARE_1:19;
       0 <= d*b by A1,SQUARE_1:19;
     then 0 + 0 <= a*c + d*b by A9,REAL_1:55;
     then 2*(a*c + d*b) <= 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
)) by A8,SQUARE_1:89;
     then b^2 + 2*(a*c + d*b) <= 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2)) + b^2
       by AXIOMS:24;
     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 AXIOMS:24;
     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 AXIOMS:24;
     then a^2 + (c^2 + (d^2 + (b^2 + 2*((a*c) + (d*b))))) <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by AXIOMS:24;
     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 XCMPLX_1:8;
     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 XCMPLX_1:1;
     then a^2 + (c^2 + (2*(a*c) + (d^2 + (b^2 + 2*(d*b))))) <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
     then a^2 + ((c^2 + (2*(a*c) + (d^2 + b^2 + 2*(d*b))))) <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
     then a^2 + ((2*(a*c) +c^2) + (d^2 + b^2 + 2*(d*b))) <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
     then (a^2 + (2*(a*c) + c^2)) + (d^2 + b^2 + 2*(d*b)) <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
     then (a^2 + (2*(a*c) + c^2)) + (d^2 + (2*(d*b) + b^2)) <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
     then (a^2 + 2*(a*c) + c^2) + (d^2 + (2*(d*b) + b^2)) <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
     then (a^2 + 2*(a*c) + c^2) + (d^2 + 2*(d*b) + b^2) <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:1;
     then (a^2 + 2*a*c + c^2) + (d^2 + 2*(d*b) + b^2) <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:4;
     then (a^2 + 2*a*c + c^2) + (d^2 + 2*d*b + b^2) <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by XCMPLX_1:4;
     then (a + c)^2 + (d^2 + 2*d*b + b^2) <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by SQUARE_1:63;
     then (a + c)^2 +(d + b)^2 <=
      a^2 + (c^2 + (d^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2
))))) by SQUARE_1:63;
     then (a + c)^2 + (d + b)^2 <=
      a^2 + ((b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2))) + (c^2 + d^2
)) by XCMPLX_1:1;
     then (a + c)^2 + (d + b)^2 <=
      (a^2 + (b^2 + 2*(sqrt(a^2 + b^2)*sqrt(d^2 + c^2)))) + (c^2 + d^2
) by XCMPLX_1:1;
     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
) by XCMPLX_1:1;
     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 4;
     then (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 A7,SQUARE_1:def 4;
     then (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 XCMPLX_1:4;
     then A10: (a + c)^2 + (d + b)^2 <=
       (sqrt(a^2 + b^2) + sqrt(c^2 + d^2))^2 by SQUARE_1:63;
     A11: 0 <= (a + c)^2 by SQUARE_1:72;
       0 <= (d + b)^2 by SQUARE_1:72;
     then 0 + 0 <= (a + c)^2 + (d + b)^2 by A11,REAL_1:55;
     then A12: sqrt((a + c)^2 + (d + b)^2) <=
                   sqrt((sqrt(a^2 + b^2) + sqrt(c^2 + d^2))^2
) by A10,SQUARE_1:94;
     A13: 0 <= sqrt(a^2 + b^2) by A5,SQUARE_1:def 4;
       0 <= sqrt(c^2 + d^2) by A7,SQUARE_1:def 4;
     then 0 + 0 <= sqrt(a^2 + b^2) + sqrt(c^2 + d^2) by A13,REAL_1:55;
     hence thesis by A12,SQUARE_1:89;
     end;

   theorem Th6:
    for x,y,z being Element of [:the carrier of X,the carrier of Y:]
            st (x = [x1,x2] & y = [y1,y2] & z = [z1,z2]) holds
    dist_cart2S(X,Y).(x,z) <= dist_cart2S(X,Y).(x,y) + dist_cart2S(X,Y).(y,z)
     proof
      let x,y,z be Element of [:the carrier of X,the carrier of Y:] such that
      A1:x = [x1,x2] & y = [y1,y2] & z = [z1,z2];
      set d1 = dist(x1,z1);
      set d2 = dist(x1,y1);
      set d3 = dist(y1,z1);
      set d4 = dist(x2,z2);
      set d5 = dist(x2,y2);
      set d6 = dist(y2,z2);
      A2: d1 <= d2 + d3 by METRIC_1:4;
        0 <= d1 by METRIC_1:5;
      then A3: (d1)^2 <= (d2 + d3)^2 by A2,SQUARE_1:77;
      A4: d4 <= d5 + d6 by METRIC_1:4;
        0 <= d4 by METRIC_1:5;
      then (d4)^2 <= (d5 + d6)^2 by A4,SQUARE_1:77;
      then A5: (d1)^2 + (d4)^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A3,REAL_1:55;
      A6: 0 <= (d1)^2 by SQUARE_1:72;
        0 <= (d4)^2 by SQUARE_1:72;
      then 0 + 0 <= (d1)^2 + (d4)^2 by A6,REAL_1:55;
      then A7: sqrt((d1)^2 + (d4)^2)<= sqrt((d2 + d3)^2 + (d5 + d6)^2)
        by A5,SQUARE_1:94;
        (0 <= d2 & 0 <= d3 & 0 <= d5 & 0 <= d6) by METRIC_1:5;
      then sqrt((d2 + d3)^2 + (d5 + d6)^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2
 + d6^2)
        by Th5;
      then sqrt((d1)^2 + (d4)^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2 + d6^2)
        by A7,AXIOMS:22;
      then dist_cart2S(X,Y).(x,z) <=
                 sqrt((d2)^2 + (d5)^2) + sqrt((d3)^2 + (d6)^2) by A1,Def1;
      then dist_cart2S(X,Y).(x,z) <=
             dist_cart2S(X,Y).(x,y) + sqrt((d3)^2 + (d6)^2) by A1,Def1;
      hence thesis by A1,Def1;
     end;

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

   definition let X,Y;
     func MetrSpaceCart2S(X,Y) -> strict non empty MetrSpace equals :Def3:
      MetrStruct(#[:the carrier of X,the carrier of Y:],dist_cart2S(X,Y)#);
    coherence
     proof
         now
        let x,y,z be Element of
        MetrStruct(#[:the carrier of X,the carrier of Y:],dist_cart2S(X,Y)#);
        reconsider x' = x,y' = y ,z' = z as Element of
        [:the carrier of X,the carrier of Y:];
        A1:ex x1,x2 st x' = [x1,x2] by DOMAIN_1:9;
        A2:ex y1,y2 st y' = [y1,y2] by DOMAIN_1:9;
        A3:ex z1,z2 st z' = [z1,z2] by DOMAIN_1:9;
        A4: dist(x,y) = dist_cart2S(X,Y).(x',y') by METRIC_1:def 1;
        A5: dist(x,z) = dist_cart2S(X,Y).(x',z') by METRIC_1:def 1;
        A6: dist(y,z) = dist_cart2S(X,Y).(y',z') by METRIC_1:def 1;
        A7: dist(y,x) = dist_cart2S(X,Y).(y',x') by METRIC_1:def 1;
        thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th3;
        thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th4;
        thus dist(x,z) <= dist(x,y) + dist(y,z)
        by A1,A2,A3,A4,A5,A6,Th6;
        end;
      hence thesis by METRIC_1:6;
      end;
    end;

canceled;

theorem
      MetrStruct(# [:the carrier of X,the carrier of Y:],dist_cart2S(X,Y)#)
     is MetrSpace
  proof
    MetrStruct(# [:the carrier of X,the carrier of Y:],dist_cart2S(X,Y)#) =
  MetrSpaceCart2S(X,Y) by Def3;
  hence thesis;
  end;

begin
:: METRICS IN THE CARTESIAN PRODUCT OF THREE SETS

reserve Z for non empty MetrSpace;
reserve x3,y3,z3 for Element of Z;

definition let X,Y,Z;
  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
  :Def4: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
    proof
     deffunc G(Element of X,Element of X,
               Element of Y,Element of Y,
               Element of Z,Element of Z)
               = 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] = G(x1,y1,x2,y2,x3,y3) from LambdaMCART1;
        take F;
      let x1,y1 be Element of X,
          x2,y2 be Element of Y,
          x3,y3 be Element of Z,
          x,y be Element of
          [:the carrier of X,the carrier of Y,the carrier of Z:] such that
          A2: ( x = [x1,x2,x3] & y = [y1,y2,y3] );
      thus F.(x,y) = F.[x,y] by BINOP_1:def 1
       .= sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))^2) by A1,A2;
     end;
   uniqueness
    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;

    assume that
    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
       f1.(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))^2) and
    A4: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
);
      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:];
        consider x1 be Element of X,
                      x2 be Element of Y,
                      x3 be Element of Z
        such that
        A5: x = [x1,x2,x3] by DOMAIN_1:15;
        consider y1 be Element of X,
                      y2 be Element of Y,
                      y3 be Element of Z
        such that
        A6: y = [y1,y2,y3] by DOMAIN_1:15;
        thus f1.(x,y) =
        sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))^2) by A3,A5,A6
                     .= f2.(x,y) by A4,A5,A6;
       end;
   hence thesis by BINOP_1:2;
    end;
   end;

canceled;

   theorem Th10:
    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
    dist_cart3S(X,Y,Z).(x,y) = 0 iff x = y
     proof
      let x,y be Element of
              [:the carrier of X,the carrier of Y,the carrier of Z:] such that
      A1:x = [x1,x2,x3] & y = [y1,y2,y3];
      thus dist_cart3S(X,Y,Z).(x,y) = 0 implies x = y
       proof
        assume A2:dist_cart3S(X,Y,Z).(x,y) = 0;
        set d1 = dist(x1,y1);
        set d2 = dist(x2,y2);
        set d3 = dist(x3,y3);
          sqrt(d1^2 + d2^2 + d3^2) = 0 by A1,A2,Def4;
        then A3: sqrt(d1^2 + (d2^2 + d3^2)) = 0 by XCMPLX_1:1;
        A4: 0 <= d1^2 by SQUARE_1:72;
        A5: 0 <= d2^2 by SQUARE_1:72;
          0 <= d3^2 by SQUARE_1:72;
        then A6: 0 + 0 <= d2^2 + d3^2 by A5,REAL_1:55;
        then d1^2 = 0 & (d2^2 + d3^2) = 0 by A3,A4,Th2;
        then d1 = 0 by SQUARE_1:73;
        then A7: x1 = y1 by METRIC_1:2;
        A8: d2^2 + d3^2 = 0 by A3,A4,A6,Th2;
        A9: 0 <= d2^2 by SQUARE_1:72;
A10:        0 <= d3^2 by SQUARE_1:72;
        then A11: d2^2 = 0 & d3^2 = 0 by A8,A9,METRIC_3:2;
          d2^2 = 0 by A8,A9,A10,METRIC_3:2;
        then d2 = 0 by SQUARE_1:73;
        then A12:x2 = y2 by METRIC_1:2;
          d3 = 0 by A11,SQUARE_1:73;
        hence thesis by A1,A7,A12,METRIC_1:2;
        end;
        assume x = y;
        then A13:x1 = y1 & x2 = y2 & x3 = y3 by A1,MCART_1:28;
        then A14: (dist(x1,y1))^2 = 0 by METRIC_1:1,SQUARE_1:60;
A15:    (dist(x2,y2))^2 = 0 by A13,METRIC_1:1,SQUARE_1:60;
          dist_cart3S(X,Y,Z).(x,y) =
         sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))^2) by A1,Def4
               .= 0 by A13,A14,A15,METRIC_1:1,SQUARE_1:60,82;
        hence thesis;
        end;

   theorem Th11:
    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
    dist_cart3S(X,Y,Z).(x,y) = dist_cart3S(X,Y,Z).(y,x)
     proof
      let x,y be Element of
      [:the carrier of X,the carrier of Y,the carrier of Z:]; assume
      A1:x = [x1,x2,x3] & y = [y1,y2,y3];
      then dist_cart3S(X,Y,Z).(x,y) =
 sqrt((dist(y1,x1))^2 + (dist(y2,x2))^2 + (dist(y3,x3))^2) by Def4
              .= dist_cart3S(X,Y,Z).(y,x) by A1,Def4;
      hence thesis;
     end;

   theorem Th12:
   for a,b,c being Element of REAL holds
   (a + b + c)^2 = a^2 + b^2 + c^2 + (2*a*b + 2*a*c + 2*b*c)
    proof
   let a,b,c be Element of REAL;
      (a + b + c)^2 = (a + (b + c))^2 by XCMPLX_1:1
                .= a^2 + 2*a*(b + c) + (b + c)^2 by SQUARE_1:63
                .= a^2 + 2*a*(b + c) + (b^2 + 2*b*c + c^2) by SQUARE_1:63
                .= a^2 + 2*a*(b + c) + (b^2 + (c^2 + 2*b*c)) by XCMPLX_1:1
                .= ((a^2 + 2*a*(b + c)) + b^2) + (c^2 + 2*b*c) by XCMPLX_1:1
                .= ((a^2 + b^2) + 2*a*(b + c)) + (c^2 + 2*b*c) by XCMPLX_1:1
                .= ((a^2 + b^2) + 2*a*(b + c)) + c^2 + 2*b*c by XCMPLX_1:1
                .= (((a^2 + b^2) + c^2) + 2*a*(b + c)) + 2*b*c by XCMPLX_1:1
                .= ((a^2 + b^2) + c^2) + (2*a*(b + c) + 2*b*c) by XCMPLX_1:1
                .= ((a^2 + b^2) + c^2
) + ((2*a*b + 2*a*c) + 2*b*c) by XCMPLX_1:8;
     hence thesis;
    end;

   theorem Th13:
    for a,b,c,d,e,f being Element of REAL 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 Element of REAL;
     A1:0 <= ((a*d) - (c*b))^2 by SQUARE_1:72;
     A2:0 <= ((a*f) - (e*c))^2 by SQUARE_1:72;
       0 <= ((b*f) - (e*d))^2 by SQUARE_1:72;
     then 0 + 0 <= ((a*f) - (e*c))^2 + ((b*f) - (e*d))^2
              by A2,REAL_1:55;
     then 0 + 0 <= ((a*d) - (c*b))^2 + (((a*f) - (e*c))^2 + ((b*f) - (e*d))^2)
              by A1,REAL_1:55;
     then 0 <= ((a*d) - (c*b))^2 + ((a*f) - (e*c))^2 + ((b*f) - (e*d))^2
              by XCMPLX_1:1;
     then 0 <= ((a*d)^2 - 2*(a*d)*(c*b) + (c*b)^2) +
              ((a*f) - (e*c))^2 + ((b*f) - (e*d))^2 by SQUARE_1:64;
     then 0 <= ((a*d)^2 + (-2*(a*d)*(c*b)) + (c*b)^2) +
              ((a*f) - (e*c))^2 + ((b*f) - (e*d))^2 by XCMPLX_0:def 8;
     then 0 <= ((a*d)^2 + (c*b)^2) + (-2*(a*d)*(c*b)) +
              ((a*f) - (e*c))^2 + ((b*f) - (e*d))^2 by XCMPLX_1:1;
     then 0 <= ((a*d)^2 + (c*b)^2) + ((a*f) - (e*c))^2 +
              (-2*(a*d)*(c*b)) + ((b*f) - (e*d))^2 by XCMPLX_1:1;
     then 0 <= ((a*d)^2 + (c*b)^2) + ((a*f) - (e*c))^2 +
              ((b*f) - (e*d))^2 + (-2*(a*d)*(c*b)) by XCMPLX_1:1;
     then 0 <= (((a*d)^2 + (c*b)^2) + ((a*f) - (e*c))^2 +
              ((b*f) - (e*d))^2) - 2*(a*d)*(c*b) by XCMPLX_0:def 8;
     then 0 + 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2) + ((a*f) - (e*c))^2 +
              ((b*f) - (e*d))^2 by REAL_1:84;
     then 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2) +
       ((a*f)^2 - 2*(a*f)*(e*c) + (e*c)^2) + ((b*f) - (e*d))^2 by SQUARE_1:64;
     then 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2) +
       ((a*f)^2 + (- 2*(a*f)*(e*c)) + (e*c)^2) + ((b*f) - (e*d))^2
 by XCMPLX_0:def 8
;
     then 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2) +
       (((a*f)^2 + (e*c)^2) + (- 2*(a*f)*(e*c))) + ((b*f) - (e*d))^2
 by XCMPLX_1:1;
     then 2*(a*d)*(c*b) <= ((a*d)^2 + (c*b)^2) +
       ((a*f)^2 + (e*c)^2) + (- 2*(a*f)*(e*c)) + ((b*f) - (e*d))^2
 by XCMPLX_1:1;
     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)) by XCMPLX_1:1;
     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)) by XCMPLX_1:1;
     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) by XCMPLX_0:def 8;
     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) - (e*d))^2 by REAL_1:84;
     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 - 2*(b*f)*(e*d) + (e*d)^2
) by SQUARE_1:64;
     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 + (- 2*(b*f)*(e*d)) + (e*d)^2
) by XCMPLX_0:def 8;
     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 XCMPLX_1:1;
     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 XCMPLX_1:1;
     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 XCMPLX_1:1;
     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 XCMPLX_0:def 8;
     hence thesis by REAL_1:84;
     end;

    theorem Th14:
    for a,b,c,d,e,f being Element of REAL holds
       (((((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2))
     + (e^2*d^2)) + (e^2*f^2)) + (b^2*d^2)) + (a^2*c^2) =
       (a^2 + b^2 + e^2)*(c^2 + d^2 + f^2)
    proof
     let a,b,c,d,e,f be Element of REAL;
       (((((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2)) + (e^2*
d
^2))
        + (e^2*f^2)) + (b^2*d^2)) + (a^2*c^2)
     = ((((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2)) + (e^2*d
^2))
        + (e^2*f^2)) + (a^2*c^2) + (b^2*d^2) by XCMPLX_1:1
     .= (((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2)) + (e^2*d
^2))
        + (a^2*c^2) + (e^2*f^2) + (b^2*d^2) by XCMPLX_1:1
     .= (((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2)) + (e^2*d
^2))
        + (a^2*c^2) + (b^2*d^2) + (e^2*f^2) by XCMPLX_1:1
     .= ((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2)) + (e^2*d
^2)
        + ((a^2*c^2) + (b^2*d^2)) + (e^2*f^2) by XCMPLX_1:1
     .= ((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2))
        + ((a^2*c^2) + (b^2*d^2)) + (e^2*d^2) + (e^2*f^2) by XCMPLX_1:1
     .= ((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2))
        + ((a^2*c^2) + (b^2*d^2)) + ((e^2*d^2) + (e^2*f^2)) by XCMPLX_1:1
     .= ((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2))
        + ((a^2*c^2) + (b^2*d^2)) + (e^2*(d^2 + f^2)) by XCMPLX_1:8
     .= (a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (b^2*f^2) + (e^2*c^2)
        + ((a^2*c^2) + (b^2*d^2)) + e^2*(d^2 + f^2) by XCMPLX_1:1
     .= (a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (b^2*f^2) + ((a^2*c^2) + (b^2*d^2
))
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
     .= (a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + ((a^2*c^2) + (b^2*d^2)) + (b^2*f
^2)
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
     .= (a^2*d^2) + ((a^2*c^2) + (b^2*d^2)) + ((a^2*f^2) + (c^2*b^2)) + (b^2*f
^2)
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
     .= (a^2*d^2) + (a^2*c^2) + (b^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (b^2*f^2)
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
     .= (a^2*d^2) + (a^2*c^2) + (b^2*d^2) + (a^2*f^2) + (c^2*b^2) + (b^2*f^2)
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
     .= ((a^2*c^2) + (a^2*d^2)) + (a^2*f^2) + (b^2*d^2) + (c^2*b^2) + (b^2*f^2)
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
     .= (a^2*(c^2 + d^2)) + (a^2*f^2) + (b^2*d^2) + (c^2*b^2) + (b^2*f^2)
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:8
     .= (a^2*((c^2 + d^2) + f^2)) + (b^2*d^2) + (c^2*b^2) + (b^2*f^2)
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:8
     .= a^2*((c^2 + d^2) + f^2) + ((b^2*c^2) + (b^2*d^2)) + (b^2*f^2)
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
     .= a^2*((c^2 + d^2) + f^2) + (b^2*(c^2 + d^2)) + (b^2*f^2)
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:8
     .= a^2*((c^2 + d^2) + f^2) + (b^2*(c^2 + d^2) + (b^2*f^2))
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:1
     .= a^2*((c^2 + d^2) + f^2) + (b^2*((c^2 + d^2) + f^2))
        + (e^2*c^2) + e^2*(d^2 + f^2) by XCMPLX_1:8
     .= a^2*((c^2 + d^2) + f^2) + (b^2*((c^2 + d^2) + f^2))
        + ((e^2*c^2) + e^2*(d^2 + f^2)) by XCMPLX_1:1
     .= a^2*((c^2 + d^2) + f^2) + (b^2*((c^2 + d^2) + f^2)) + (e^2*(c^2 + (d^2
 + f^2)))
        by XCMPLX_1:8
     .= ((a^2 + b^2)*((c^2 + d^2) + f^2)) + e^2*(c^2 + (d^2 + f^2
)) by XCMPLX_1:8
     .= (a^2 + b^2)*((c^2 + d^2) + f^2) + e^2*(c^2 + d^2 + f^2) by XCMPLX_1:1
     .= (((a^2 + b^2) + e^2)*((c^2 + d^2) + f^2)) by XCMPLX_1:8;
     hence thesis;
    end;

   theorem Th15:
    for a,b,c,d,e,f being Element of REAL 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 Element of REAL;
        (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 Th13;
     then ((2*(a*d)*(c*b)) + (2*(a*f)*(e*c)) + (2*((b*f)*(d*e)))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*(a*d)*(c*b)) + (2*(a*f)*(e*c)) + (2*(((b*f)*d)*e))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*(a*d)*(c*b)) + (2*(a*f)*(e*c)) + (2*(((b*d)*f)*e))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*(a*d)*(c*b)) + (2*(a*f)*(e*c)) + (2*((b*d)*(e*f)))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*(a*d)*(c*b)) + (2*((a*f)*(c*e))) + (2*((b*d)*(e*f)))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*(a*d)*(c*b)) + (2*(((a*f)*c)*e)) + (2*((b*d)*(e*f)))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*(a*d)*(c*b)) + (2*(((a*c)*f)*e)) + (2*((b*d)*(e*f)))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*(a*d)*(c*b)) + (2*((a*c)*(f*e))) + (2*((b*d)*(e*f)))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*(a*d)*(c*b)) + (2*((a*c)*(f*e))) + (2*(b*d)*(e*f))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*(a*d)*(c*b)) + (2*(a*c)*(f*e)) + (2*(b*d)*(e*f))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*((a*d)*(b*c))) + (2*(a*c)*(f*e)) + (2*(b*d)*(e*f))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*(((a*d)*b)*c)) + (2*(a*c)*(f*e)) + (2*(b*d)*(e*f))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*(((a*b)*d)*c)) + (2*(a*c)*(f*e)) + (2*(b*d)*(e*f))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((2*((a*b)*(c*d))) + (2*(a*c)*(f*e)) + (2*(b*d)*(e*f))) <=
      (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2
) by XCMPLX_1:4;
     then ((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
) by XCMPLX_1:4;
     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 AXIOMS:24;
     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 AXIOMS:24;
     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 AXIOMS:24;
     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 XCMPLX_1:1;
     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 XCMPLX_1:1;
     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 XCMPLX_1:4;
     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 XCMPLX_1:4;
     then (a*c)^2 + (b*d)^2 + (e*f)^2 + (2*(((a*c)*b)*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 XCMPLX_1:4;
     then (a*c)^2 + (b*d)^2 + (e*f)^2 + (2*((a*c)*(b*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 XCMPLX_1:4;
     then (a*c)^2 + (b*d)^2 + (e*f)^2 + (2*(a*c)*(b*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 XCMPLX_1:4;
     then A1:((a*c) + (b*d) + (e*f))^2 <= (((((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 Th12;
     set a1 = ((a*c) + (b*d) + (e*f))^2;
       a1 <= (((((a^2*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 A1,SQUARE_1:68;
     then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a*f)^2 + (e*c)^2 + (b*f)^2)
     + (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
     then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e*c)^2 + (b*f)^2)
     + (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
     then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b*f)^2)
     + (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
     then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b^2*f^2))
     + (e*d)^2) + (e*f)^2) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
     then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b^2*f^2))
     + (e^2*d^2)) + (e*f)^2) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
     then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b^2*f^2))
     + (e^2*d^2)) + (e^2*f^2)) + (b*d)^2) + (a*c)^2 by SQUARE_1:68;
     then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b^2*f^2))
     + (e^2*d^2)) + (e^2*f^2)) + (b^2*d^2)) + (a*c)^2 by SQUARE_1:68;
     then a1 <= (((((a^2*d^2) + (c^2*b^2) + (a^2*f^2) + (e^2*c^2) + (b^2*f^2))
     + (e^2*d^2)) + (e^2*f^2)) + (b^2*d^2)) + (a^2*c^2) by SQUARE_1:68;
     then a1 <= (((((a^2*d^2) + ((a^2*f^2) + (c^2*b^2)) + (e^2*c^2) + (b^2*f^2
))
     + (e^2*d^2)) + (e^2*f^2)) + (b^2*d^2)) + (a^2*c^2) by XCMPLX_1:1;
     hence thesis by Th14;
      end;

    Lm1:
    for a,b,c,d,e,f being Element of REAL
       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 Element of REAL; assume
     A1: 0 <= a & 0 <= b & 0 <= c & 0 <= d & 0 <= e & 0 <= f;
     A2: ((a*c) + (b*d) + (e*f))^2 <= (a^2 + b^2 + e^2)*(c^2 + d^2 + f^2
) by Th15;
       0 <= ((a*c) + (b*d) + (e*f))^2 by SQUARE_1:72;
     then A3: sqrt(((a*c) + (b*d) + (e*f))^2) <=
       sqrt((a^2 + b^2 + e^2)*(c^2 + d^2 + f^2)) by A2,SQUARE_1:94;
     A4: 0 <= a*c by A1,SQUARE_1:19;
     A5: 0 <= b*d by A1,SQUARE_1:19;
       0 <= e*f by A1,SQUARE_1:19;
     then 0 + 0 <= b*d + e*f by A5,REAL_1:55;
     then 0 + 0 <= a*c + (b*d + e*f) by A4,REAL_1:55;
     then 0 <= a*c + b*d + e*f by XCMPLX_1:1;
     then A6: ((a*c) + (b*d) + (e*f)) <= sqrt((a^2 + b^2 + e^2)*(c^2 + d^2 + f
^2))
          by A3,SQUARE_1:89;
     A7: 0 <= a^2 by SQUARE_1:72;
       0 <= b^2 by SQUARE_1:72;
     then A8: 0 + 0 <= a^2 + b^2 by A7,REAL_1:55;

       0 <= e^2 by SQUARE_1:72;
     then A9: 0 + 0 <= (a^2 + b^2) + e^2 by A8,REAL_1:55;

     A10: 0 <= c^2 by SQUARE_1:72;
       0 <= d^2 by SQUARE_1:72;
     then A11: 0 + 0 <= c^2 + d^2 by A10,REAL_1:55;

       0 <= f^2 by SQUARE_1:72;
     then A12: 0 + 0 <= (c^2 + d^2) + f^2 by A11,REAL_1:55;
     then ((a*c) + (b*d) + (e*f)) <= sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f
^2)
          by A6,A9,SQUARE_1:97;
     then 2*((a*c) + (b*d) + (e*f)) <=
       2*(sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) by AXIOMS:25;
     then 2*(((a*c) + (b*d)) + (e*f)) <=
       2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2) by XCMPLX_1:4;
     then (2*((a*c) + (b*d)) + 2*(e*f)) <=
       2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2) by XCMPLX_1:8;
     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 AXIOMS:24;
     then (2*((a*c) + (b*d))) + (e^2 + 2*(e*f))
           <= (2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2)) + e^2
 by XCMPLX_1:1;
     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 AXIOMS:24;
     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 XCMPLX_1:1;
     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 XCMPLX_1:4;
     then (2*((a*c) + (b*d))) + ((e + f)^2)
      <= ((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
 by SQUARE_1:63;
     then (2*(a*c) + 2*(b*d)) + ((e + f)^2)
      <= ((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
 by XCMPLX_1:8;
     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 AXIOMS:24;
     then ((2*(a*c) + 2*(b*d)) + b^2) + (e + f)^2
           <= (((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
) + b^2 by XCMPLX_1:1;
     then (2*(a*c) + (b^2 + 2*(b*d))) + (e + f)^2
           <= (((e^2 + 2*sqrt(a^2 + b^2 + e^2)*sqrt(c^2 + d^2 + f^2))) + f^2
) + b^2 by XCMPLX_1:1;
     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 AXIOMS:24;
     then ((2*(a*c) + (b^2 + 2*(b*d))) + d^2) + (e + f)^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 XCMPLX_1:1;
     then (2*(a*c) + (b^2 + 2*(b*d) + d^2)) + (e + f)^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 XCMPLX_1:1;
     then (2*(a*c) + (b^2 + 2*b*d + d^2)) + (e + f)^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 XCMPLX_1:4;
     then (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))) + f^2
)) + d^2
by SQUARE_1:63;
     then 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))) + f^2
)) + d^2
             by XCMPLX_1:1;
     then 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))) + f^2
) + d^2)
             by XCMPLX_1:1;
     then 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)) by XCMPLX_1:1;
     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 AXIOMS:24;
     then (a^2 + 2*(a*c)) + ((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)) + (d^2 + f^2
)))
             by XCMPLX_1:1;
     then (a^2 + 2*(a*c)) + ((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)) + (d^2 + f^2))
             by XCMPLX_1:1;
     then (a^2 + 2*(a*c)) + ((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))) + (d^2 + f^2)
             by XCMPLX_1:1;
     then (a^2 + 2*(a*c)) + ((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)) + (d^2 + f^2
) by XCMPLX_1:1;
     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 AXIOMS:24;
     then ((a^2 + 2*(a*c) + 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)) + (d^2 + f^2
)) + c^2
             by XCMPLX_1:1;
     then ((a^2 + 2*a*c + 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)) + (d^2 + f^2
)) + c^2
             by XCMPLX_1:4;
     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)) + (d^2 + f^2
)) + c^2 by SQUARE_1:63;
     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)) + (d^2 + f^2
)) + c^2
             by XCMPLX_1:1;
     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)) by XCMPLX_1:1;
     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)
       by XCMPLX_1:1;
     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 A9,SQUARE_1:def 4;
     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)) + (sqrt(c^2 + d^2
 + f^2))^2
          by A12,SQUARE_1:def 4;
     then A13: ((a + c)^2 + (b + d)^2 + (e + f)^2) <= (sqrt(a^2 + b^2 + e^2)
          + sqrt(c^2 + d^2 + f^2))^2 by SQUARE_1:63;
     A14: 0 <= (a + c)^2 by SQUARE_1:72;
       0 <= (b + d)^2 by SQUARE_1:72;
     then A15: 0 + 0 <= (a + c)^2 + (b + d)^2 by A14,REAL_1:55;
       0 <= (e + f)^2 by SQUARE_1:72;
     then 0 + 0 <= ((a + c)^2 + (b + d)^2) + (e + f)^2 by A15,REAL_1:55;
     then A16: 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 A13,SQUARE_1:94;
     A17: 0 <= sqrt(a^2 + b^2 + e^2) by A9,SQUARE_1:def 4;
       0 <= sqrt(c^2 + d^2 + f^2) by A12,SQUARE_1:def 4;
     then 0 + 0 <= (sqrt(a^2 + b^2 + e^2) + sqrt(c^2 + d^2 + f^2
)) by A17,REAL_1:55;
     hence thesis by A16,SQUARE_1:89;
     end;

   theorem
    Th16:
    for x,y,z being Element of
       [:the carrier of X,the carrier of Y,the carrier of Z:]
            st (x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3]) 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 Element of
      [:the carrier of X,the carrier of Y,the carrier of Z:] such that
      A1:x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3];
      set d1 = dist(x1,z1), d2 = dist(x1,y1), d3 = dist(y1,z1);
      set d4 = dist(x2,z2), d5 = dist(x2,y2), d6 = dist(y2,z2);
      set d7 = dist(x3,z3), d8 = dist(x3,y3), d9 = dist(y3,z3);
      A2: d1 <= d2 + d3 by METRIC_1:4;
        0 <= d1 by METRIC_1:5;
      then A3: (d1)^2 <= (d2 + d3)^2 by A2,SQUARE_1:77;
      A4: d4 <= d5 + d6 by METRIC_1:4;
        0 <= d4 by METRIC_1:5;
      then A5: (d4)^2 <= (d5 + d6)^2 by A4,SQUARE_1:77;
      A6: d7 <= d8 + d9 by METRIC_1:4;
        0 <= d7 by METRIC_1:5;
      then A7: (d7)^2 <= (d8 + d9)^2 by A6,SQUARE_1:77;
        (d1)^2 + (d4)^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A3,A5,REAL_1:55;
      then A8: (d1)^2 + (d4)^2 + (d7)^2 <= (d2 + d3)^2 + (d5 + d6)^2
 + (d8 + d9)^2
by A7,REAL_1:55;
      A9: 0 <= (d1)^2 by SQUARE_1:72;
        0 <= (d4)^2 by SQUARE_1:72;
      then A10: 0 + 0 <= (d1)^2 + (d4)^2 by A9,REAL_1:55;
        0 <= (d7)^2 by SQUARE_1:72;
      then 0 + 0 <= ((d1)^2 + (d4)^2) + (d7)^2 by A10,REAL_1:55;
      then A11: sqrt((d1)^2 + (d4)^2 + (d7)^2) <= sqrt((d2 + d3)^2 + (d5 + d6)
^2 +
               (d8 + d9)^2) by A8,SQUARE_1:94;
        (0 <= d2 & 0 <= d3 & 0 <= d5 & 0 <= d6 & 0 <= d8 & 0 <= d9)
           by METRIC_1:5;
      then sqrt((d2 + d3)^2 + (d5 + d6)^2 + (d8 + d9)^2) <= sqrt(d2^2 + d5^2
 + d8^2)
           + sqrt(d3^2 + d6^2 + d9^2) by Lm1;
      then sqrt((d1)^2 + (d4)^2 + d7^2) <=
        sqrt(d2^2 + d5^2 + d8^2) + sqrt(d3^2 + d6^2 + d9^2) by A11,AXIOMS:22;
      then dist_cart3S(X,Y,Z).(x,z) <=
            sqrt((d2)^2 + (d5)^2 + d8^2) + sqrt((d3)^2 + (d6)^2 + d9^2
) by A1,Def4;
      then dist_cart3S(X,Y,Z).(x,z) <=
         dist_cart3S(X,Y,Z).(x,y) + sqrt((d3)^2 + (d6)^2 + d9^2) by A1,Def4;
      hence thesis by A1,Def4;
     end;

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

   definition let X,Y,Z;
     func MetrSpaceCart3S(X,Y,Z) -> strict non empty MetrSpace equals :Def6:
      MetrStruct(#[:the carrier of X,the carrier of Y,the carrier of Z:],
     dist_cart3S(X,Y,Z)#);
    coherence
     proof
         now
        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)#);
        reconsider x' = x,y' = y ,z' = z as Element of
        [:the carrier of X,the carrier of Y,the carrier of Z:];
        A1:ex x1,x2,x3 st x' = [x1,x2,x3] by DOMAIN_1:15;
        A2:ex y1,y2,y3 st y' = [y1,y2,y3] by DOMAIN_1:15;
        A3:ex z1,z2,z3 st z' = [z1,z2,z3] by DOMAIN_1:15;
        A4: dist(x,y) = dist_cart3S(X,Y,Z).(x',y') by METRIC_1:def 1;
        A5: dist(x,z) = dist_cart3S(X,Y,Z).(x',z') by METRIC_1:def 1;
        A6: dist(y,z) = dist_cart3S(X,Y,Z).(y',z') by METRIC_1:def 1;
        A7: dist(y,x) = dist_cart3S(X,Y,Z).(y',x') by METRIC_1:def 1;
        thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th10;
        thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th11;
        thus dist(x,z) <= dist(x,y) + dist(y,z)
        by A1,A2,A3,A4,A5,A6,Th16;
        end;
        hence thesis by METRIC_1:6;
      end;
    end;

canceled;

theorem
    MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:],
  dist_cart3S(X,Y,Z)#)
  is MetrSpace
  proof
    MetrStruct (# [:the carrier of X,the carrier of Y,the carrier of Z:],
  dist_cart3S(X,Y,Z)#) = MetrSpaceCart3S(X,Y,Z) by Def6;
  hence thesis;
  end;

reserve x1,x2,y1,y2,z1,z2 for Element of REAL;

definition
  func taxi_dist2 -> Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means
  :Def7: 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
   proof
    deffunc G(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] = G(x1,y1,x2,y2) from LambdaMCART;
    take F;
      let x1,y1,x2,y2 be Element of REAL,
          x,y be Element of [:REAL,REAL:] such that
          A2: ( x = [x1,x2] & y = [y1,y2] );
      thus F.(x,y) = F.[x,y] by BINOP_1:def 1
                  .= real_dist.(x1,y1) + real_dist.(x2,y2) by A1,A2;
     end;
   uniqueness
    proof
    let f1,f2 be Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL;
    assume that
    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
           f1.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) and
    A4: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);
      for x,y being Element of [:REAL,REAL:]
        holds f1.(x,y) = f2.(x,y)
       proof
        let x,y be Element of [:REAL,REAL:];
        consider x1 be Element of REAL,
                      x2 be Element of REAL
        such that
        A5: x = [x1,x2] by DOMAIN_1:9;
        consider y1 be Element of REAL,
                      y2 be Element of REAL
        such that
        A6: y = [y1,y2] by DOMAIN_1:9;
        thus f1.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) by A3,A5,A6
                     .= f2.(x,y) by A4,A5,A6;
       end;
   hence thesis by BINOP_1:2;
    end;
  end;

   theorem Th19:
    for x1,x2,y1,y2 being Element of REAL
    for x,y being Element of [:REAL,REAL:]
            st (x = [x1,x2] & y = [y1,y2]) holds
    taxi_dist2.(x,y) = 0 iff x = y
     proof
      let x1,x2,y1,y2 be Element of REAL,
      x,y be Element of [:REAL,REAL:] such that
      A1:x = [x1,x2] & y = [y1,y2];
      thus taxi_dist2.(x,y) = 0 implies x = y
       proof
        assume A2:taxi_dist2.(x,y) = 0;
        set d1 = real_dist.(x1,y1);
        set d2 = real_dist.(x2,y2);
        A3: d1 + d2 = 0 by A1,A2,Def7;
          d1 = abs(x1 - y1) by METRIC_1:def 13;
        then A4: 0 <= d1 by ABSVALUE:5;
          d2 = abs(x2 - y2) by METRIC_1:def 13;
        then A5: 0 <= d2 by ABSVALUE:5;
        then A6:d1 = 0 & d2 = 0 by A3,A4,METRIC_3:2;
          d1 = 0 by A3,A4,A5,METRIC_3:2;
        then x1 = y1 by METRIC_1:9;
        hence thesis by A1,A6,METRIC_1:9;
        end;
        assume x = y;
        then A7:x1 = y1 & x2 = y2 by A1,ZFMISC_1:33;
        then A8:real_dist.(x2,y2) = 0 by METRIC_1:9;
          taxi_dist2.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) by A1,Def7
                            .= 0 by A7,A8,METRIC_1:9;
        hence thesis;
        end;

   theorem Th20:
    for x,y being Element of [:REAL,REAL:]
            st (x = [x1,x2] & y = [y1,y2]) holds
    taxi_dist2.(x,y) = taxi_dist2.(y,x)
     proof
      let x,y be Element of [:REAL,REAL:]; assume
      A1:x = [x1,x2] & y = [y1,y2];
      then taxi_dist2.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) by Def7
                      .= real_dist.(y1,x1) + real_dist.(x2,y2) by METRIC_1:10
                      .= real_dist.(y1,x1) + real_dist.(y2,x2) by METRIC_1:10
                          .= taxi_dist2.(y,x) by A1,Def7;
      hence thesis;
     end;

   theorem
    Th21:
    for x,y,z being Element of [:REAL,REAL:]
            st (x = [x1,x2] & y = [y1,y2] & z = [z1,z2]) holds
    taxi_dist2.(x,z) <= taxi_dist2.(x,y) + taxi_dist2.(y,z)
     proof
      let x,y,z be Element of [:REAL,REAL:] such that
      A1:x = [x1,x2] & y = [y1,y2] & z = [z1,z2];
      set d1 = real_dist.(x1,z1);
      set d2 = real_dist.(x1,y1);
      set d3 = real_dist.(y1,z1);
      set d4 = real_dist.(x2,z2);
      set d5 = real_dist.(x2,y2);
      set d6 = real_dist.(y2,z2);
A2:      (d2 + d3) + (d5 + d6) = ((d2 + d3) + d5) + d6 by XCMPLX_1:1
                          .= ((d2 + d5) + d3) + d6 by XCMPLX_1:1
                          .= (d2 + d5) + (d3 + d6) by XCMPLX_1:1
                          .= taxi_dist2.(x,y) + (d3 +d6) by A1,Def7
                          .= taxi_dist2.(x,y) + taxi_dist2.(y,z) by A1,Def7;
      A3: d1 <= d2 + d3 by METRIC_1:11;
      A4: d4 <= d5 + d6 by METRIC_1:11;
        taxi_dist2.(x,z) = d1 + d4 by A1,Def7;
      hence thesis by A2,A3,A4,REAL_1:55;
     end;

   definition
     func RealSpaceCart2 -> strict non empty MetrSpace equals
        MetrStruct(#[:REAL,REAL:],taxi_dist2#);
    coherence
     proof
         now
        let x,y,z be Element of
        MetrStruct(#[:REAL,REAL:],taxi_dist2#);
        reconsider x' = x,y' = y ,z' = z as Element of [:REAL,REAL:];
        A1:ex x1,x2 st x' = [x1,x2] by DOMAIN_1:9;
        A2:ex y1,y2 st y' = [y1,y2] by DOMAIN_1:9;
        A3:ex z1,z2 st z' = [z1,z2] by DOMAIN_1:9;
        A4: dist(x,y) = taxi_dist2.(x',y') by METRIC_1:def 1;
        A5: dist(x,z) = taxi_dist2.(x',z') by METRIC_1:def 1;
        A6: dist(y,z) = taxi_dist2.(y',z') by METRIC_1:def 1;
        A7: dist(y,x) = taxi_dist2.(y',x') by METRIC_1:def 1;
        thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th19;
        thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th20;
        thus dist(x,z) <= dist(x,y) + dist(y,z)
                         by A1,A2,A3,A4,A5,A6,Th21;
        end;
      hence thesis by METRIC_1:6;
      end;
    end;

definition
  func Eukl_dist2 -> Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means
  :Def9: 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
   proof
    deffunc G(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] = G(x1,y1,x2,y2)
            from LambdaMCART;
    take F;
      let x1,y1,x2,y2 be Element of REAL,
          x,y be Element of [:REAL,REAL:] such that
          A2: ( x = [x1,x2] & y = [y1,y2] );
      thus F.(x,y) = F.[x,y] by BINOP_1:def 1
       .= sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)) by A1,A2;
     end;
   uniqueness
    proof
    let f1,f2 be Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL;
    assume that
    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
           f1.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)) and
    A4: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));
      for x,y being Element of [:REAL,REAL:]
        holds f1.(x,y) = f2.(x,y)
       proof
        let x,y be Element of [:REAL,REAL:];
        consider x1 be Element of REAL,
                      x2 be Element of REAL such that
        A5: x = [x1,x2] by DOMAIN_1:9;
        consider y1 be Element of REAL,
                      y2 be Element of REAL such that
        A6: y = [y1,y2] by DOMAIN_1:9;
     thus f1.(x,y)=sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2))
       by A3,A5,A6
                     .= f2.(x,y) by A4,A5,A6;
       end;
   hence thesis by BINOP_1:2;
    end;
  end;

   theorem Th22:
    for x1,x2,y1,y2 being Element of REAL
    for x,y being Element of [:REAL,REAL:]
            st (x = [x1,x2] & y = [y1,y2]) holds
    Eukl_dist2.(x,y) = 0 iff x = y
     proof
      let x1,x2,y1,y2 be Element of REAL,
      x,y be Element of [:REAL,REAL:] such that
      A1:x = [x1,x2] & y = [y1,y2];
      thus Eukl_dist2.(x,y) = 0 implies x = y
       proof
        assume A2:Eukl_dist2.(x,y) = 0;
        set d1 = real_dist.(x1,y1);
        set d2 = real_dist.(x2,y2);
        A3:sqrt(d1^2 + d2^2) = 0 by A1,A2,Def9;
        A4: 0 <= d1^2 by SQUARE_1:72;
A5:        0 <= d2^2 by SQUARE_1:72;
        then A6:d1^2 = 0 & d2^2 = 0 by A3,A4,Th2;
          d1^2 = 0 by A3,A4,A5,Th2;
        then d1 = 0 by SQUARE_1:73;
        then A7: x1 = y1 by METRIC_1:9;
          d2 = 0 by A6,SQUARE_1:73;
        hence thesis by A1,A7,METRIC_1:9;
       end;
        assume x = y;
        then A8:x1 = y1 & x2 = y2 by A1,ZFMISC_1:33;
        then A9:(real_dist.(x1,y1))^2 = 0 by METRIC_1:9,SQUARE_1:60;
        A10: (real_dist.(x2,y2))^2 = 0 by A8,METRIC_1:9,SQUARE_1:60;
          Eukl_dist2.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2))^2
)
                                                   by A1,Def9
                              .= 0 by A9,A10,Th2;
        hence thesis;
        end;

   theorem Th23:
    for x,y being Element of [:REAL,REAL:]
            st (x = [x1,x2] & y = [y1,y2]) holds
    Eukl_dist2.(x,y) = Eukl_dist2.(y,x)
     proof
      let x,y be Element of [:REAL,REAL:]; assume
      A1:x = [x1,x2] & y = [y1,y2];
      then Eukl_dist2.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)
^2
))
                         by Def9
      .= sqrt((real_dist.(y1,x1))^2 + (real_dist.(x2,y2)^2)) by METRIC_1:10
      .= sqrt((real_dist.(y1,x1))^2 + (real_dist.(y2,x2)^2)) by METRIC_1:10
      .= Eukl_dist2.(y,x) by A1,Def9;
      hence thesis;
     end;

   theorem
    Th24:
    for x,y,z being Element of [:REAL,REAL:]
            st (x = [x1,x2] & y = [y1,y2] & z = [z1,z2]) holds
    Eukl_dist2.(x,z) <= Eukl_dist2.(x,y) + Eukl_dist2.(y,z)
     proof
      let x,y,z be Element of [:REAL,REAL:] such that
      A1:x = [x1,x2] & y = [y1,y2] & z = [z1,z2];
      set d1 = real_dist.(x1,z1);
      set d2 = real_dist.(x1,y1);
      set d3 = real_dist.(y1,z1);
      set d4 = real_dist.(x2,z2);
      set d5 = real_dist.(x2,y2);
      set d6 = real_dist.(y2,z2);
      A2: d1 <= d2 + d3 by METRIC_1:11;
        d1 = abs(x1 - z1) by METRIC_1:def 13;
      then 0 <= d1 by ABSVALUE:5;
      then A3: (d1)^2 <= (d2 + d3)^2 by A2,SQUARE_1:77;
      A4: d4 <= d5 + d6 by METRIC_1:11;
        d4 = abs(x2 - z2) by METRIC_1:def 13;
      then 0 <= d4 by ABSVALUE:5;
      then (d4)^2 <= (d5 + d6)^2 by A4,SQUARE_1:77;
      then A5: (d1)^2 + (d4)^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A3,REAL_1:55;
      A6: 0 <= (d1)^2 by SQUARE_1:72;
        0 <= (d4)^2 by SQUARE_1:72;
      then 0 + 0 <= (d1)^2 + (d4)^2 by A6,REAL_1:55;
      then A7: sqrt((d1)^2 + (d4)^2)<= sqrt((d2 + d3)^2 + (d5 + d6)^2)
        by A5,SQUARE_1:94;
A8:      d2 = abs(x1 - y1) by METRIC_1:def 13;
A9:      d3 = abs(y1 - z1) by METRIC_1:def 13;
A10:     d5 = abs(x2 - y2) by METRIC_1:def 13;
        d6 = abs(y2 - z2) by METRIC_1:def 13;
      then (0 <= d2 & 0 <= d3 & 0 <= d5 & 0 <= d6) by A8,A9,A10,ABSVALUE:5;
      then sqrt((d2 + d3)^2 + (d5 + d6)^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2
 + d6^2)
        by Th5;
      then sqrt((d1)^2 + (d4)^2) <= sqrt(d2^2 + d5^2) + sqrt(d3^2 + d6^2)
        by A7,AXIOMS:22;
      then Eukl_dist2.(x,z) <=
                 sqrt((d2)^2 + (d5)^2) + sqrt((d3)^2 + (d6)^2) by A1,Def9;
      then Eukl_dist2.(x,z) <=
             Eukl_dist2.(x,y) + sqrt((d3)^2 + (d6)^2) by A1,Def9;
      hence thesis by A1,Def9;
     end;

   definition
     func EuklSpace2 -> strict non empty MetrSpace equals
        MetrStruct(#[:REAL,REAL:],Eukl_dist2#);
    coherence
     proof
         now
        let x,y,z be Element of
          MetrStruct(#[:REAL,REAL:],Eukl_dist2#);
        reconsider x' = x,y' = y ,z' = z as Element of [:REAL,REAL:];
        A1:ex x1,x2 st x' = [x1,x2] by DOMAIN_1:9;
        A2:ex y1,y2 st y' = [y1,y2] by DOMAIN_1:9;
        A3:ex z1,z2 st z' = [z1,z2] by DOMAIN_1:9;
        A4: dist(x,y) = Eukl_dist2.(x',y') by METRIC_1:def 1;
        A5: dist(x,z) = Eukl_dist2.(x',z') by METRIC_1:def 1;
        A6: dist(y,z) = Eukl_dist2.(y',z') by METRIC_1:def 1;
        A7: dist(y,x) = Eukl_dist2.(y',x') by METRIC_1:def 1;
        thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th22;
        thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th23;
        thus dist(x,z) <= dist(x,y) + dist(y,z)
                         by A1,A2,A3,A4,A5,A6,Th24;
        end;
      hence thesis by METRIC_1:6;
      end;
    end;

reserve x3,y3,z3 for Element of REAL;

definition
  func taxi_dist3 -> Function of [:[:REAL,REAL,REAL:],
                                   [:REAL,REAL,REAL:]:],REAL means
  :Def11: 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
   proof
    deffunc G(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] = G(x1,y1,x2,y2,x3,y3) from LambdaMCART1;
    take F;
      let x1,y1,x2,y2,x3,y3 be Element of REAL,
          x,y be Element of [:REAL,REAL,REAL:] such that
          A2: ( x = [x1,x2,x3] & y = [y1,y2,y3] );
      thus F.(x,y) = F.[x,y] by BINOP_1:def 1
                  .= real_dist.(x1,y1) + real_dist.(x2,y2) + real_dist.(x3,y3)
                  by A1,A2;
     end;
   uniqueness
    proof
    let f1,f2 be Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL;
    assume that
    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
           f1.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) + real_dist.(x3,y3)
           and
    A4: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);
      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:];
        consider x1 be Element of REAL,x2 be Element of REAL,
                      x3 be Element of REAL
        such that
        A5: x = [x1,x2,x3] by DOMAIN_1:15;
        consider y1 be Element of REAL,y2 be Element of REAL,
                      y3 be Element of REAL
        such that
        A6: y = [y1,y2,y3] by DOMAIN_1:15;
      thus f1.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) + real_dist.(x3,y3
)
                       by A3,A5,A6
                    .= f2.(x,y) by A4,A5,A6;
       end;
   hence thesis by BINOP_1:2;
    end;
end;
   theorem
    Th25:
    for x1,x2,y1,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
    taxi_dist3.(x,y) = 0 iff x = y
     proof
      let x1,x2,y1,y2,x3,y3 be Element of REAL,
      x,y be Element of [:REAL,REAL,REAL:] such that
      A1:x = [x1,x2,x3] & y = [y1,y2,y3];
      thus taxi_dist3.(x,y) = 0 implies x = y
       proof
        assume A2:taxi_dist3.(x,y) = 0;
        set d1 = real_dist.(x1,y1);
        set d2 = real_dist.(x2,y2);
        set d3 = real_dist.(x3,y3);
        set d4 = d1 + d2;
        A3: d4 + d3 = 0 by A1,A2,Def11;
          d3 = abs(x3 - y3) by METRIC_1:def 13;
        then A4: 0 <= d3 by ABSVALUE:5;
          d2 = abs(x2 - y2) by METRIC_1:def 13;
        then A5: 0 <= d2 by ABSVALUE:5;
          d1 = abs(x1 - y1) by METRIC_1:def 13;
        then A6: 0 <= d1 by ABSVALUE:5;
        then A7: 0 + 0 <= d1 + d2 by A5,REAL_1:55;

        then A8:d4 = 0 & d3 = 0 by A3,A4,METRIC_3:2;
          d4 = 0 by A3,A4,A7,METRIC_3:2;
        then A9:d1 = 0 & d2 = 0 by A5,A6,METRIC_3:2;
        A10: x3 = y3 by A8,METRIC_1:9;
           x1 = y1 by A9,METRIC_1:9;
        hence thesis by A1,A9,A10,METRIC_1:9;
        end;
        assume A11: x = y;
        then A12: (x1 = y1 & x2 = y2) & x3 = y3 by A1,MCART_1:28;
        A13: x1 = y1 & (x2 = y2 & x3 = y3) by A1,A11,MCART_1:28;
        A14:real_dist.(x1,y1) = 0 by A12,METRIC_1:9;
        A15:real_dist.(x2,y2) = 0 by A12,METRIC_1:9;
          taxi_dist3.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2)
                           + real_dist.(x3,y3) by A1,Def11
                         .= 0 by A13,A14,A15,METRIC_1:9;
        hence thesis;
        end;

   theorem
    Th26:
    for x,y being Element of [:REAL,REAL,REAL:]
            st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
    taxi_dist3.(x,y) = taxi_dist3.(y,x)
     proof
      let x,y be Element of [:REAL,REAL,REAL:]; assume
      A1:x = [x1,x2,x3] & y = [y1,y2,y3];
      then taxi_dist3.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2)
                         + real_dist.(x3,y3) by Def11
                      .= real_dist.(y1,x1) + real_dist.(x2,y2)
                         + real_dist.(x3,y3) by METRIC_1:10
                      .= real_dist.(y1,x1) + real_dist.(y2,x2)
                         + real_dist.(x3,y3) by METRIC_1:10
                      .= real_dist.(y1,x1) + real_dist.(y2,x2)
                         + real_dist.(y3,x3) by METRIC_1:10
                      .= taxi_dist3.(y,x) by A1,Def11;
      hence thesis;
     end;

   theorem
    Th27:
    for x,y,z being Element of [:REAL,REAL,REAL:]
            st (x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3]) holds
    taxi_dist3.(x,z) <= taxi_dist3.(x,y) + taxi_dist3.(y,z)
     proof
      let x,y,z be Element of [:REAL,REAL,REAL:] such that
      A1:x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3];
      set d1 = real_dist.(x1,z1);
      set d2 = real_dist.(x1,y1);
      set d3 = real_dist.(y1,z1);
      set d4 = real_dist.(x2,z2);
      set d5 = real_dist.(x2,y2);
      set d6 = real_dist.(y2,z2);
      set d7 = real_dist.(x3,z3);
      set d8 = real_dist.(x3,y3);
      set d9 = real_dist.(y3,z3);
A2:      ((d2 + d3) + (d5 + d6)) + (d8 + d9)
                    = (((d2 + d3) + d5) + d6) + (d8 + d9) by XCMPLX_1:1
                   .= (((d2 + d5) + d3) + d6) + (d8 + d9) by XCMPLX_1:1
                   .= ((d2 + d5) + (d3 + d6)) + (d8 + d9) by XCMPLX_1:1
                   .= ((d2 + d5) + (d8 + d9)) + (d3 + d6) by XCMPLX_1:1
                   .= (((d2 + d5) + d8) + d9) + (d3 + d6) by XCMPLX_1:1
                   .= ((d2 + d5) + d8) + ((d3 + d6) + d9) by XCMPLX_1:1
                   .= taxi_dist3.(x,y) + ((d3 +d6) + d9) by A1,Def11
                   .= taxi_dist3.(x,y) + taxi_dist3.(y,z) by A1,Def11;
      A3: d1 <= d2 + d3 by METRIC_1:11;
      A4: d4 <= d5 + d6 by METRIC_1:11;
      set d10 = d1 + d4;
      A5: d10 <= (d2 + d3) + (d5 + d6) by A3,A4,REAL_1:55;
        d7 <= d8 + d9 by METRIC_1:11;
      then d10 + d7 <= ((d2 + d3) + (d5 + d6)) + (d8 + d9) by A5,REAL_1:55;
      hence thesis by A1,A2,Def11;
     end;

   definition
     func RealSpaceCart3 -> strict non empty MetrSpace equals
        MetrStruct(#[:REAL,REAL,REAL:],taxi_dist3#);
    coherence
     proof
         now
        let x,y,z be Element of
          MetrStruct(#[:REAL,REAL,REAL:],taxi_dist3#);
        reconsider x' = x,y' = y ,z' = z as Element of [:REAL,REAL,REAL:];
        A1:ex x1,x2,x3 st x' = [x1,x2,x3] by DOMAIN_1:15;
        A2:ex y1,y2,y3 st y' = [y1,y2,y3] by DOMAIN_1:15;
        A3:ex z1,z2,z3 st z' = [z1,z2,z3] by DOMAIN_1:15;
        A4: dist(x,y) = taxi_dist3.(x',y') by METRIC_1:def 1;
        A5: dist(x,z) = taxi_dist3.(x',z') by METRIC_1:def 1;
        A6: dist(y,z) = taxi_dist3.(y',z') by METRIC_1:def 1;
        A7: dist(y,x) = taxi_dist3.(y',x') by METRIC_1:def 1;
        thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th25;
        thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th26;
        thus dist(x,z) <= dist(x,y) + dist(y,z)
                         by A1,A2,A3,A4,A5,A6,Th27;
        end;
      hence thesis by METRIC_1:6;
      end;
    end;

definition
  func Eukl_dist3 -> Function of [:[:REAL,REAL,REAL:],
                                   [:REAL,REAL,REAL:]:],REAL means
  :Def13: 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
   proof
    deffunc G(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] = G(x1,y1,x2,y2,x3,y3) from LambdaMCART1;
    take F;
      let x1,y1,x2,y2,x3,y3 be Element of REAL,
          x,y be Element of [:REAL,REAL,REAL:] such that
          A2: ( x = [x1,x2,x3] & y = [y1,y2,y3] );
      thus F.(x,y) = F.[x,y] by BINOP_1:def 1
                  .= sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)
                     + (real_dist.(x3,y3)^2)) by A1,A2;
     end;
   uniqueness
    proof
    let f1,f2 be Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL;
    assume that
    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
           f1.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)
                      + (real_dist.(x3,y3)^2)) and
    A4: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));
      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:];
        consider x1 be Element of REAL,
                      x2 be Element of REAL,
                      x3 be Element of REAL
        such that
        A5: x = [x1,x2,x3] by DOMAIN_1:15;
        consider y1 be Element of REAL,
                      y2 be Element of REAL,
                      y3 be Element of REAL
        such that
        A6: y = [y1,y2,y3] by DOMAIN_1:15;
     thus f1.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)
                     + (real_dist.(x3,y3)^2)) by A3,A5,A6
                   .= f2.(x,y) by A4,A5,A6;
       end;
   hence thesis by BINOP_1:2;
    end;
  end;

   theorem Th28:
    for x1,x2,y1,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
    Eukl_dist3.(x,y) = 0 iff x = y
     proof
      let x1,x2,y1,y2,x3,y3 be Element of REAL,
      x,y be Element of [:REAL,REAL,REAL:] such that
      A1:x = [x1,x2,x3] & y = [y1,y2,y3];
      thus Eukl_dist3.(x,y) = 0 implies x = y
       proof
        assume A2:Eukl_dist3.(x,y) = 0;
        set d1 = real_dist.(x1,y1);
        set d2 = real_dist.(x2,y2);
        set d3 = real_dist.(x3,y3);
          sqrt(d1^2 + d2^2 + d3^2) = 0 by A1,A2,Def13;
        then A3:sqrt(d1^2 + (d2^2 + d3^2)) =0 by XCMPLX_1:1;
        A4: 0 <= d1^2 by SQUARE_1:72;
        A5: 0 <= d2^2 by SQUARE_1:72;
          0 <= d3^2 by SQUARE_1:72;
        then A6: 0 + 0 <= d2^2 + d3^2 by A5,REAL_1:55;
        then d1^2 = 0 & (d2^2 + d3^2) = 0 by A3,A4,Th2;
        then d1 = 0 by SQUARE_1:73;
        then A7: x1 = y1 by METRIC_1:9;
        A8: d2^2 + d3^2 = 0 by A3,A4,A6,Th2;
        A9: 0 <= d2^2 by SQUARE_1:72;
A10:        0 <= d3^2 by SQUARE_1:72;
        then A11: d2^2 = 0 & d3^2 = 0 by A8,A9,METRIC_3:2;
          d2^2 = 0 by A8,A9,A10,METRIC_3:2;
        then d2 = 0 by SQUARE_1:73;
        then A12:x2 = y2 by METRIC_1:9;
          d3 = 0 by A11,SQUARE_1:73;
        hence thesis by A1,A7,A12,METRIC_1:9;
        end;
        assume x = y;
        then A13:x1 = y1 & x2 = y2 & x3 = y3 by A1,MCART_1:28;
        then A14: (real_dist.(x1,y1))^2 = 0 by METRIC_1:9,SQUARE_1:60;
A15:         (real_dist.(x2,y2))^2 = 0 by A13,METRIC_1:9,SQUARE_1:60;
          Eukl_dist3.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2))^2
                           + (real_dist.(x3,y3))^2) by A1,Def13
                    .= 0 by A13,A14,A15,METRIC_1:9,SQUARE_1:60,82;
        hence thesis;
        end;

   theorem Th29:
    for x,y being Element of [:REAL,REAL,REAL:]
            st (x = [x1,x2,x3] & y = [y1,y2,y3]) holds
    Eukl_dist3.(x,y) = Eukl_dist3.(y,x)
     proof
      let x,y be Element of [:REAL,REAL,REAL:]; assume
      A1:x = [x1,x2,x3] & y = [y1,y2,y3];
      then Eukl_dist3.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)
^2
)
                         + (real_dist.(x3,y3)^2)) by Def13
              .= sqrt((real_dist.(y1,x1))^2 + (real_dist.(x2,y2)^2)
                 + (real_dist.(x3,y3)^2)) by METRIC_1:10
              .= sqrt((real_dist.(y1,x1))^2 + (real_dist.(y2,x2)^2)
                 + (real_dist.(x3,y3)^2)) by METRIC_1:10
              .= sqrt((real_dist.(y1,x1))^2 + (real_dist.(y2,x2)^2)
                 + (real_dist.(y3,x3)^2)) by METRIC_1:10
                .= Eukl_dist3.(y,x) by A1,Def13;
      hence thesis;
     end;

   theorem Th30:
    for x,y,z being Element of [:REAL,REAL,REAL:]
            st (x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3]) holds
    Eukl_dist3.(x,z) <= Eukl_dist3.(x,y) + Eukl_dist3.(y,z)
     proof
      let x,y,z be Element of [:REAL,REAL,REAL:] such that
      A1:x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3];
      set d1 = real_dist.(x1,z1), d2 = real_dist.(x1,y1);
      set d3 = real_dist.(y1,z1), d4 = real_dist.(x2,z2);
      set d5 = real_dist.(x2,y2), d6 = real_dist.(y2,z2);
      set d7 = real_dist.(x3,z3), d8 = real_dist.(x3,y3);
      set d9 = real_dist.(y3,z3);
      A2: d1 <= d2 + d3 by METRIC_1:11;
        d1 = abs(x1 - z1) by METRIC_1:def 13;
      then 0 <= d1 by ABSVALUE:5;
      then A3: (d1)^2 <= (d2 + d3)^2 by A2,SQUARE_1:77;
      A4: d4 <= d5 + d6 by METRIC_1:11;
        d4 = abs(x2 - z2) by METRIC_1:def 13;
      then 0 <= d4 by ABSVALUE:5;
      then A5: (d4)^2 <= (d5 + d6)^2 by A4,SQUARE_1:77;
      A6: d7 <= d8 + d9 by METRIC_1:11;
        d7 = abs(x3 - z3) by METRIC_1:def 13;
      then 0 <= d7 by ABSVALUE:5;
      then A7: (d7)^2 <= (d8 + d9)^2 by A6,SQUARE_1:77;
        (d1)^2 + (d4)^2 <= (d2 + d3)^2 + (d5 + d6)^2 by A3,A5,REAL_1:55;
      then A8: (d1)^2 + (d4)^2 + (d7)^2 <= (d2 + d3)^2 + (d5 + d6)^2
 + (d8 + d9)^2
by A7,REAL_1:55;
      A9: 0 <= (d1)^2 by SQUARE_1:72;
        0 <= (d4)^2 by SQUARE_1:72;
      then A10: 0 + 0 <= (d1)^2 + (d4)^2 by A9,REAL_1:55;
        0 <= (d7)^2 by SQUARE_1:72;
      then 0 + 0 <= ((d1)^2 + (d4)^2) + (d7)^2 by A10,REAL_1:55;
      then A11: sqrt((d1)^2 + (d4)^2 + (d7)^2) <= sqrt((d2 + d3)^2 + (d5 + d6)
^2 +
               (d8 + d9)^2) by A8,SQUARE_1:94;
A12:      d2 = abs(x1 - y1) by METRIC_1:def 13;
A13:      d3 = abs(y1 - z1) by METRIC_1:def 13;
A14:      d5 = abs(x2 - y2) by METRIC_1:def 13;
A15:      d6 = abs(y2 - z2) by METRIC_1:def 13;
A16:      d8 = abs(x3 - y3) by METRIC_1:def 13;
        d9 = abs(y3 - z3) by METRIC_1:def 13;
      then (0 <= d2 & 0 <= d3 & 0 <= d5 & 0 <= d6 & 0 <= d8 & 0 <= d9)
           by A12,A13,A14,A15,A16,ABSVALUE:5;
      then sqrt((d2 + d3)^2 + (d5 + d6)^2 + (d8 + d9)^2) <= sqrt(d2^2 + d5^2
 + d8^2)
           + sqrt(d3^2 + d6^2 + d9^2) by Lm1;
      then sqrt((d1)^2 + (d4)^2 + d7^2) <= sqrt(d2^2 + d5^2 + d8^2) +
       sqrt(d3^2 + d6^2 + d9^2)
           by A11,AXIOMS:22;
      then Eukl_dist3.(x,z) <=
            sqrt((d2)^2 + (d5)^2 + d8^2) + sqrt((d3)^2 + (d6)^2 + d9^2
) by A1,Def13;
      then Eukl_dist3.(x,z) <=
         Eukl_dist3.(x,y) + sqrt((d3)^2 + (d6)^2 + d9^2) by A1,Def13;
      hence thesis by A1,Def13;
     end;

   definition
     func EuklSpace3 -> strict non empty MetrSpace equals
        MetrStruct(#[:REAL,REAL,REAL:],Eukl_dist3#);
    coherence
     proof
         now
        let x,y,z be Element of
         MetrStruct(#[:REAL,REAL,REAL:],Eukl_dist3#);
        reconsider x' = x,y' = y ,z' = z as Element of [:REAL,REAL,REAL:];
        A1:ex x1,x2,x3 st x' = [x1,x2,x3] by DOMAIN_1:15;
        A2:ex y1,y2,y3 st y' = [y1,y2,y3] by DOMAIN_1:15;
        A3:ex z1,z2,z3 st z' = [z1,z2,z3] by DOMAIN_1:15;
        A4: dist(x,y) = Eukl_dist3.(x',y') by METRIC_1:def 1;
        A5: dist(x,z) = Eukl_dist3.(x',z') by METRIC_1:def 1;
        A6: dist(y,z) = Eukl_dist3.(y',z') by METRIC_1:def 1;
        A7: dist(y,x) = Eukl_dist3.(y',x') by METRIC_1:def 1;
        thus dist(x,y) = 0 iff x = y by A1,A2,A4,Th28;
        thus dist(x,y) = dist(y,x) by A1,A2,A4,A7,Th29;
        thus dist(x,z) <= dist(x,y) + dist(y,z)
                         by A1,A2,A3,A4,A5,A6,Th30;
        end;
      hence thesis by METRIC_1:6;
      end;
    end;

Back to top