let x, y be Element of [:REAL ,REAL :]; :: thesis: 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 by MCART_1:10;
A1: ( x = [x1,x2] & y = [y1,y2] ) by MCART_1:24;
then taxi_dist2 . x,y = (real_dist . x1,y1) + (real_dist . x2,y2) by Def7
.= (real_dist . y1,x1) + (real_dist . x2,y2) by METRIC_1:10
.= (real_dist . y1,x1) + (real_dist . y2,x2) by METRIC_1:10
.= taxi_dist2 . y,x by A1, Def7 ;
hence taxi_dist2 . x,y = taxi_dist2 . y,x ; :: thesis: verum