set XX = [:X,(the carrier of M \ {a}):] \/ {[X,a]};
defpred S₁[ set , set , set ] means for x, y being Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]} st x = $1 & y = $2 holds
for x1, y1 being set
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies $3 = dist x2,y2 ) & ( x1 <> y1 implies $3 = (dist x2,a) + (dist a,y2) ) );
A1: 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
ex z being set st
( z in REAL & S₁[x,y,z] )

proof

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 ex z being set st
( z in REAL & S₁[x,y,z] ) )
assume A2: ( x in [:X,(the carrier of M \ {a}):] \/ {[X,a]} & y in [:X,(the carrier of M \ {a}):] \/ {[X,a]} ) ; :: thesis: ex z being set st
( z in REAL & S₁[x,y,z] )
consider x1 being set , x2 being Point of M such that
A3: ( x = [x1,x2] & ( ( x1 in X & x2 <> a ) or ( x1 = X & x2 = a ) ) ) by A2, Th38;
consider y1 being set , y2 being Point of M such that
A4: ( y = [y1,y2] & ( ( y1 in X & y2 <> a ) or ( y1 = X & y2 = a ) ) ) by A2, Th38;

now

per cases ( x1 = y1 or x1 <> y1 ) ;

suppose A5: x1 = y1 ; :: thesis: ex d being Element of REAL st
( d in REAL & ( for x', y' being Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]} st x' = x & y' = y holds
for x1', y1' being set
for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) ) ) )

take d = dist x2,y2; :: thesis: ( d in REAL & ( for x', y' being Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]} st x' = x & y' = y holds
for x1', y1' being set
for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) ) ) )
thus d in REAL ; :: thesis: for x', y' being Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]} st x' = x & y' = y holds
for x1', y1' being set
for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) )
let x', y' be Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: ( x' = x & y' = y implies for x1', y1' being set
for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) ) )
assume A6: ( x' = x & y' = y ) ; :: thesis: for x1', y1' being set
for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) )
let x1', y1' be set ; :: thesis: for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) )
let x2', y2' be Point of M; :: thesis: ( x' = [x1',x2'] & y' = [y1',y2'] implies ( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) ) )
assume A7: ( x' = [x1',x2'] & y' = [y1',y2'] ) ; :: thesis: ( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) )
( x1' = x1 & x2' = x2 & y1' = y1 & y2' = y2 ) by A3, A4, A6, A7, ZFMISC_1:33;
hence ( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) ) by A5; :: thesis: verum

end;

suppose A8: x1 <> y1 ; :: thesis: ex d being Element of REAL st
( d in REAL & ( for x', y' being Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]} st x' = x & y' = y holds
for x1', y1' being set
for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) ) ) )

take d = (dist x2,a) + (dist a,y2); :: thesis: ( d in REAL & ( for x', y' being Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]} st x' = x & y' = y holds
for x1', y1' being set
for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) ) ) )
thus d in REAL ; :: thesis: for x', y' being Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]} st x' = x & y' = y holds
for x1', y1' being set
for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) )
let x', y' be Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: ( x' = x & y' = y implies for x1', y1' being set
for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) ) )
assume A9: ( x' = x & y' = y ) ; :: thesis: for x1', y1' being set
for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) )
let x1', y1' be set ; :: thesis: for x2', y2' being Point of M st x' = [x1',x2'] & y' = [y1',y2'] holds
( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) )
let x2', y2' be Point of M; :: thesis: ( x' = [x1',x2'] & y' = [y1',y2'] implies ( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) ) )
assume A10: ( x' = [x1',x2'] & y' = [y1',y2'] ) ; :: thesis: ( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) )
( x1' = x1 & x2' = x2 & y1' = y1 & y2' = y2 ) by A3, A4, A9, A10, ZFMISC_1:33;
hence ( ( x1' = y1' implies d = dist x2',y2' ) & ( x1' <> y1' implies d = (dist x2',a) + (dist a,y2') ) ) by A8; :: thesis: verum

end;

end;

end;

hence ex z being set st
( z in REAL & S₁[x,y,z] ) ; :: thesis: verum

end;

consider f being Function of [:([:X,(the carrier of M \ {a}):] \/ {[X,a]}),([:X,(the carrier of M \ {a}):] \/ {[X,a]}):],REAL such that
A11: 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
S₁[x,y,f . x,y] from BINOP_1:sch 1(A1);
take f ; :: thesis: for x, y being Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being set
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies f . x,y = dist x2,y2 ) & ( x1 <> y1 implies f . x,y = (dist x2,a) + (dist a,y2) ) )
thus for x, y being Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being set
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies f . x,y = dist x2,y2 ) & ( x1 <> y1 implies f . x,y = (dist x2,a) + (dist a,y2) ) ) by A11; :: thesis: verum