let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds |.x1.| - |.x2.| <= |.(x1 - x2).|
let x1, x2 be Element of REAL n; :: thesis: |.x1.| - |.x2.| <= |.(x1 - x2).|
reconsider R1 = x1, R2 = x2 as Element of n -tuples_on REAL ;
x1 = (R1 - R2) + R2 by RVSUM_1:43;
then |.x1.| <= |.(x1 - x2).| + |.x2.| by Th9;
hence |.x1.| - |.x2.| <= |.(x1 - x2).| by XREAL_1:20; :: thesis: verum