let x, y be Element of [:REAL,REAL:]; taxi_dist2 . (x,y) = taxi_dist2 . (y,x)
reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 as Element of REAL ;
A1:
( x = [x1,x2] & y = [y1,y2] )
;
then taxi_dist2 . (x,y) =
(real_dist . (x1,y1)) + (real_dist . (x2,y2))
by Def16
.=
(real_dist . (y1,x1)) + (real_dist . (x2,y2))
by METRIC_1:9
.=
(real_dist . (y1,x1)) + (real_dist . (y2,x2))
by METRIC_1:9
.=
taxi_dist2 . (y,x)
by A1, Def16
;
hence
taxi_dist2 . (x,y) = taxi_dist2 . (y,x)
; verum