let n be Nat; :: thesis: for x, y being Element of REAL n holds abs (x - y) = abs (y - x)
let x, y be Element of REAL n; :: thesis: abs (x - y) = abs (y - x)

now :: thesis: ( dom (abs (x - y)) = dom (abs (y - x)) & ( for i being object st i in dom (abs (x - y)) holds
(abs (x - y)) . i = (abs (y - x)) . i ) )

( 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: for i being object st i in dom (abs (x - y)) holds
(abs (x - y)) . i = (abs (y - x)) . i
thus for i being object st i in dom (abs (x - y)) holds
(abs (x - y)) . i = (abs (y - x)) . i :: thesis: verum

proof

let i be object ; :: thesis: ( i in dom (abs (x - y)) implies (abs (x - y)) . i = (abs (y - x)) . i )
assume i in dom (abs (x - y)) ; :: thesis: (abs (x - y)) . i = (abs (y - x)) . i
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: verum

end;

end;

hence abs (x - y) = abs (y - x) by FUNCT_1:def 11; :: thesis: verum