deffunc H1( Element of REAL , Element of REAL , Element of REAL , Element of REAL , Element of REAL , Element of REAL ) -> Element of REAL = In ((sqrt ((((real_dist . ($1,$2)) ^2) + ((real_dist . ($3,$4)) ^2)) + ((real_dist . ($5,$6)) ^2))),REAL);
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) = H1(x1,y1,x2,y2,x3,y3)
from METRIC_3:sch 2();
take
F
; 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) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))
let x1, y1, x2, y2, x3, y3 be 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) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))
let x, y be Element of [:REAL,REAL,REAL:]; ( x = [x1,x2,x3] & y = [y1,y2,y3] implies F . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) )
assume
( x = [x1,x2,x3] & y = [y1,y2,y3] )
; F . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))
then
F . (x,y) = H1(x1,y1,x2,y2,x3,y3)
by A1;
hence
F . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))
; verum