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