let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds |.(x1 - x2).| = |.(x2 - x1).|
let x1, x2 be Element of REAL n; :: thesis: |.(x1 - x2).| = |.(x2 - x1).|
reconsider R1 = x1, R2 = x2 as Element of n -tuples_on REAL ;
thus |.(x1 - x2).| = |.(- (R2 - R1)).| by RVSUM_1:35
.= |.(x2 - x1).| by Th7 ; :: thesis: verum