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