let F1, F2 be Function of [:(M -neighbour),(M -neighbour):],REAL; ( ( 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)
; 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 ;
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)
;
verum
end;
hence
F1 = F2
by BINOP_1:2; verum