let F1, F2 be Function of [:(M -neighbour),(M -neighbour):],REAL; :: thesis: ( ( for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
F1 . (V,Q) = dist (p,q) ) & ( for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
F2 . (V,Q) = dist (p,q) ) implies F1 = F2 )
assume that
A4: for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
F1 . (V,Q) = dist (p,q) and
A5: for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
F2 . (V,Q) = dist (p,q) ; :: thesis: F1 = F2
for V, Q being Element of M -neighbour holds F1 . (V,Q) = F2 . (V,Q)

proof

let V, Q be Element of M -neighbour ; :: thesis: F1 . (V,Q) = F2 . (V,Q)
consider p being Element of M such that
A6: V = p -neighbour by Th23;
consider q being Element of M such that
A7: Q = q -neighbour by Th23;
A8: q in Q by A7, Th9;
A9: p in V by A6, Th9;
then F1 . (V,Q) = dist (p,q) by A4, A8
.= F2 . (V,Q) by A5, A9, A8 ;
hence F1 . (V,Q) = F2 . (V,Q) ; :: thesis: verum

end;

hence F1 = F2 by BINOP_1:2; :: thesis: verum