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