deffunc H_{1}( Element of X, Element of X, Element of Y, Element of Y, Element of Z, Element of Z) -> Element of REAL = In ((((dist ($1,$2)) + (dist ($3,$4))) + (dist ($5,$6))),REAL);

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) = H_{1}(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))

then F . (x,y) = H_{1}(x1,y1,x2,y2,x3,y3)
by A1;

hence F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) ; :: thesis: verum

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) = H

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))

then F . (x,y) = H

hence F . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) ; :: thesis: verum