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
A5: 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
A6: 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
A7: V = p -neighbour by Th15;
consider q being Element of M such that
A8: Q = q -neighbour by Th15;
A9: q in Q by A8, Th4;
A10: p in V by A7, Th4;
then F1 . (V,Q) = dist (p,q) by A5, A9
.= F2 . (V,Q) by A6, A10, A9 ;
hence F1 . (V,Q) = F2 . (V,Q) ; :: thesis: verum

end;

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