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:42;
then |.x1.| <= |.(x1 + x2).| + |.x2.| by Th10;
hence |.x1.| - |.x2.| <= |.(x1 + x2).| by XREAL_1:20; :: thesis: verum