set XX = [:X,( the carrier of M \ {a}):] \/ {[X,a]};
defpred S1[ object , object , object ] 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 object
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 object 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 object st
( z in REAL & S1[x,y,z] )
proof
let x, y be object ; :: 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 object st
( z in REAL & S1[x,y,z] ) )
assume that
A2: x in [:X,( the carrier of M \ {a}):] \/ {[X,a]} and
A3: y in [:X,( the carrier of M \ {a}):] \/ {[X,a]} ; :: thesis: ex z being object st
( z in REAL & S1[x,y,z] )
consider y1 being set , y2 being Point of M such that
A4: y = [y1,y2] and
( ( y1 in X & y2 <> a ) or ( y1 = X & y2 = a ) ) by A3, Th37;
consider x1 being set , x2 being Point of M such that
A5: x = [x1,x2] and
( ( x1 in X & x2 <> a ) or ( x1 = X & x2 = a ) ) by A2, Th37;
per cases ( x1 = y1 or x1 <> y1 ) ;
suppose A6: x1 = y1 ; :: thesis: ex z being object st
( z in REAL & S1[x,y,z] )
take d = dist (x2,y2); :: thesis: ( d in REAL & S1[x,y,d] )
thus d in REAL by XREAL_0:def 1; :: thesis: S1[x,y,d]
let x9, y9 be Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: ( x9 = x & y9 = y implies for x1, y1 being object
for x2, y2 being Point of M st x9 = [x1,x2] & y9 = [y1,y2] holds
( ( x1 = y1 implies d = dist (x2,y2) ) & ( x1 <> y1 implies d = (dist (x2,a)) + (dist (a,y2)) ) ) )
assume that
A7: x9 = x and
A8: y9 = y ; :: thesis: for x1, y1 being object
for x2, y2 being Point of M st x9 = [x1,x2] & y9 = [y1,y2] holds
( ( x1 = y1 implies d = dist (x2,y2) ) & ( x1 <> y1 implies d = (dist (x2,a)) + (dist (a,y2)) ) )
let x19, y19 be object ; :: thesis: for x2, y2 being Point of M st x9 = [x19,x2] & y9 = [y19,y2] holds
( ( x19 = y19 implies d = dist (x2,y2) ) & ( x19 <> y19 implies d = (dist (x2,a)) + (dist (a,y2)) ) )
let x29, y29 be Point of M; :: thesis: ( x9 = [x19,x29] & y9 = [y19,y29] implies ( ( x19 = y19 implies d = dist (x29,y29) ) & ( x19 <> y19 implies d = (dist (x29,a)) + (dist (a,y29)) ) ) )
assume that
A9: x9 = [x19,x29] and
A10: y9 = [y19,y29] ; :: thesis: ( ( x19 = y19 implies d = dist (x29,y29) ) & ( x19 <> y19 implies d = (dist (x29,a)) + (dist (a,y29)) ) )
A11: x29 = x2 by A5, A7, A9, XTUPLE_0:1;
x19 = x1 by A5, A7, A9, XTUPLE_0:1;
hence ( ( x19 = y19 implies d = dist (x29,y29) ) & ( x19 <> y19 implies d = (dist (x29,a)) + (dist (a,y29)) ) ) by A4, A6, A8, A10, A11, XTUPLE_0:1; :: thesis: verum
end;
suppose A12: x1 <> y1 ; :: thesis: ex z being object st
( z in REAL & S1[x,y,z] )
take d = (dist (x2,a)) + (dist (a,y2)); :: thesis: ( d in REAL & S1[x,y,d] )
thus d in REAL by XREAL_0:def 1; :: thesis: S1[x,y,d]
let x9, y9 be Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: ( x9 = x & y9 = y implies for x1, y1 being object
for x2, y2 being Point of M st x9 = [x1,x2] & y9 = [y1,y2] holds
( ( x1 = y1 implies d = dist (x2,y2) ) & ( x1 <> y1 implies d = (dist (x2,a)) + (dist (a,y2)) ) ) )
assume that
A13: x9 = x and
A14: y9 = y ; :: thesis: for x1, y1 being object
for x2, y2 being Point of M st x9 = [x1,x2] & y9 = [y1,y2] holds
( ( x1 = y1 implies d = dist (x2,y2) ) & ( x1 <> y1 implies d = (dist (x2,a)) + (dist (a,y2)) ) )
let x19, y19 be object ; :: thesis: for x2, y2 being Point of M st x9 = [x19,x2] & y9 = [y19,y2] holds
( ( x19 = y19 implies d = dist (x2,y2) ) & ( x19 <> y19 implies d = (dist (x2,a)) + (dist (a,y2)) ) )
let x29, y29 be Point of M; :: thesis: ( x9 = [x19,x29] & y9 = [y19,y29] implies ( ( x19 = y19 implies d = dist (x29,y29) ) & ( x19 <> y19 implies d = (dist (x29,a)) + (dist (a,y29)) ) ) )
assume that
A15: x9 = [x19,x29] and
A16: y9 = [y19,y29] ; :: thesis: ( ( x19 = y19 implies d = dist (x29,y29) ) & ( x19 <> y19 implies d = (dist (x29,a)) + (dist (a,y29)) ) )
A17: x29 = x2 by A5, A13, A15, XTUPLE_0:1;
x19 = x1 by A5, A13, A15, XTUPLE_0:1;
hence ( ( x19 = y19 implies d = dist (x29,y29) ) & ( x19 <> y19 implies d = (dist (x29,a)) + (dist (a,y29)) ) ) by A4, A12, A14, A16, A17, XTUPLE_0:1; :: thesis: verum
end;
end;
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
A18: for x, y being object st x in [:X,( the carrier of M \ {a}):] \/ {[X,a]} & y in [:X,( the carrier of M \ {a}):] \/ {[X,a]} holds
S1[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 object
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 object
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 A18; :: thesis: verum