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