set XX = [:X,( the carrier of M \ {a}):] \/ {[X,a]};
let w1, w2 be Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL; :: thesis: ( ( for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being object
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies w1 . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies w1 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) ) & ( for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being object
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies w2 . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies w2 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) ) implies w1 = w2 )
assume that
A19: for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being object
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies w1 . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies w1 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) and
A20: for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being object
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies w2 . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies w2 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) ; :: thesis: w1 = w2

now :: thesis: for x, y being set st x in [:X,( the carrier of M \ {a}):] \/ {[X,a]} & y in [:X,( the carrier of M \ {a}):] \/ {[X,a]} holds
w1 . (x,y) = w2 . (x,y)

let x, y be set ; :: thesis: ( x in [:X,( the carrier of M \ {a}):] \/ {[X,a]} & y in [:X,( the carrier of M \ {a}):] \/ {[X,a]} implies w1 . (x,y) = w2 . (x,y) )
assume that
A21: x in [:X,( the carrier of M \ {a}):] \/ {[X,a]} and
A22: y in [:X,( the carrier of M \ {a}):] \/ {[X,a]} ; :: thesis: w1 . (x,y) = w2 . (x,y)
consider y1 being set , y2 being Point of M such that
A23: y = [y1,y2] and
( ( y1 in X & y2 <> a ) or ( y1 = X & y2 = a ) ) by A22, Th37;
consider x1 being set , x2 being Point of M such that
A24: x = [x1,x2] and
( ( x1 in X & x2 <> a ) or ( x1 = X & x2 = a ) ) by A21, Th37;
reconsider x2 = x2, y2 = y2 as Point of M ;
( x1 = y1 or x1 <> y1 ) ;
then ( ( w1 . (x,y) = dist (x2,y2) & w2 . (x,y) = dist (x2,y2) ) or ( w1 . (x,y) = (dist (x2,a)) + (dist (a,y2)) & w2 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) by A19, A20, A21, A22, A24, A23;
hence w1 . (x,y) = w2 . (x,y) ; :: thesis: verum

end;

hence w1 = w2 by BINOP_1:1; :: thesis: verum