deffunc H₁( 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 = H₁(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