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