defpred S₁[ Element of M -neighbour , Element of M -neighbour , Element of REAL ] means $1,$2 is_dst $3;
A1: for V, Q being Element of M -neighbour ex v being Element of REAL st S₁[V,Q,v] by Th52;
consider F being Function of [:(M -neighbour),(M -neighbour):],REAL such that
A2: for V, Q being Element of M -neighbour holds S₁[V,Q,F . (V,Q)] from BINOP_1:sch 3(A1);
take F ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( p in V & q in Q implies F . (V,Q) = dist (p,q) )
assume A3: ( p in V & q in Q ) ; :: thesis: F . (V,Q) = dist (p,q)
V,Q is_dst F . (V,Q) by A2;
hence F . (V,Q) = dist (p,q) by A3, Def5; :: thesis: verum