deffunc H₁( Element of REAL , 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) = H₁(x1,y1,x2,y2) from METRIC_3:sch 1();
take F ; :: thesis: 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) = (real_dist . (x1,y1)) + (real_dist . (x2,y2))
let x1, y1, x2, y2 be Element of REAL ; :: thesis: for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds
F . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2))
let x, y be Element of [:REAL,REAL:]; :: thesis: ( x = [x1,x2] & y = [y1,y2] implies F . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) )
assume ( x = [x1,x2] & y = [y1,y2] ) ; :: thesis: F . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2))
hence F . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) by A1; :: thesis: verum