let n be Nat; :: thesis:
let x, y be Element of REAL n; :: thesis:

( dom (abs (x - y)) = Seg n & dom (abs (y - x)) = Seg n ) by FINSEQ_2:124;
hence dom (abs (x - y)) = dom (abs (y - x)) ; :: thesis:
thus for i being object st i in dom (abs (x - y)) holds
(abs (x - y)) . i = (abs (y - x)) . i :: thesis:

let i be object ; :: thesis:
assume i in dom (abs (x - y)) ; :: thesis:
reconsider fxy = x - y, fyx = y - x as complex-valued Function ;
A1: ( (abs fxy) . i = |.((x - y) . i).| & (abs fyx) . i = |.((y - x) . i).| ) by VALUED_1:18;
reconsider j = i as set by TARSKI:1;
reconsider rx = x, ry = y as Element of n -tuples_on REAL ;
A2: ( (rx - ry) . j = (rx . j) - (ry . j) & - ((ry - rx) . j) = - ((ry . j) - (rx . j)) ) by RVSUM_1:27;
reconsider c1 = (x - y) . i, c2 = (y - x) . i as ExtReal ;
A3: ( |.c2.| = |.(- c2).| & c1 = - c2 ) by A2, XXREAL_3:def 3, EXTREAL1:29;
( |.c1.| = |.((x - y) . i).| & |.c2.| = |.((y - x) . i).| ) by EXTREAL1:12;
hence (abs (x - y)) . i = (abs (y - x)) . i by A1, A3; :: thesis:

end;