let x, y be Element of [:REAL,REAL:]; :: thesis: Eukl_dist2 . (x,y) = Eukl_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 Eukl_dist2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) by Def18

.= sqrt (((real_dist . (y1,x1)) ^2) + ((real_dist . (x2,y2)) ^2)) by METRIC_1:9

.= sqrt (((real_dist . (y1,x1)) ^2) + ((real_dist . (y2,x2)) ^2)) by METRIC_1:9

.= Eukl_dist2 . (y,x) by A1, Def18 ;

hence Eukl_dist2 . (x,y) = Eukl_dist2 . (y,x) ; :: thesis: verum

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 Eukl_dist2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) by Def18

.= sqrt (((real_dist . (y1,x1)) ^2) + ((real_dist . (x2,y2)) ^2)) by METRIC_1:9

.= sqrt (((real_dist . (y1,x1)) ^2) + ((real_dist . (y2,x2)) ^2)) by METRIC_1:9

.= Eukl_dist2 . (y,x) by A1, Def18 ;

hence Eukl_dist2 . (x,y) = Eukl_dist2 . (y,x) ; :: thesis: verum