defpred S1[ Element of M -neighbour , Element of M -neighbour , Real] means $1,$2 is_dst $3;
A1:
for V, Q being Element of M -neighbour ex v being Element of REAL st S1[V,Q,v]
consider F being Function of [:(M -neighbour),(M -neighbour):],REAL such that
A3:
for V, Q being Element of M -neighbour holds S1[V,Q,F . (V,Q)]
from BINOP_1:sch 3(A1);
take
F
; for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
F . (V,Q) = dist (p,q)
let V, Q be Element of M -neighbour ; for p, q being Element of M st p in V & q in Q holds
F . (V,Q) = dist (p,q)
let p, q be Element of M; ( p in V & q in Q implies F . (V,Q) = dist (p,q) )
assume A4:
( p in V & q in Q )
; F . (V,Q) = dist (p,q)
V,Q is_dst F . (V,Q)
by A3;
hence
F . (V,Q) = dist (p,q)
by A4; verum