let x, y be real-valued FinSequence; :: thesis: ( len x = len y implies |.(x + y).| <= |.x.| + |.y.| )

assume A1: len x = len y ; :: thesis: |.(x + y).| <= |.x.| + |.y.|

then ( |(x,y)| <= |.|(x,y)|.| & |.|(x,y)|.| <= |.x.| * |.y.| ) by Th14, ABSVALUE:4;

then |(x,y)| <= |.x.| * |.y.| by XXREAL_0:2;

then 2 * |(x,y)| <= 2 * (|.x.| * |.y.|) by XREAL_1:64;

then A2: (|.x.| ^2) + (2 * |(x,y)|) <= (|.x.| ^2) + (2 * (|.x.| * |.y.|)) by XREAL_1:7;

|.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) by A1, Th10;

then A3: |.(x + y).| ^2 <= ((|.x.| ^2) + ((2 * |.x.|) * |.y.|)) + (|.y.| ^2) by A2, XREAL_1:7;

0 <= |.(x + y).| ^2 by XREAL_1:63;

then sqrt (|.(x + y).| ^2) <= sqrt ((|.x.| + |.y.|) ^2) by A3, SQUARE_1:26;

then A4: |.(x + y).| <= sqrt ((|.x.| + |.y.|) ^2) by EUCLID:9, SQUARE_1:22;

( 0 <= |.x.| & 0 <= |.y.| ) by EUCLID:9;

then 0 + 0 <= |.x.| + |.y.| by XREAL_1:7;

hence |.(x + y).| <= |.x.| + |.y.| by A4, SQUARE_1:22; :: thesis: verum

assume A1: len x = len y ; :: thesis: |.(x + y).| <= |.x.| + |.y.|

then ( |(x,y)| <= |.|(x,y)|.| & |.|(x,y)|.| <= |.x.| * |.y.| ) by Th14, ABSVALUE:4;

then |(x,y)| <= |.x.| * |.y.| by XXREAL_0:2;

then 2 * |(x,y)| <= 2 * (|.x.| * |.y.|) by XREAL_1:64;

then A2: (|.x.| ^2) + (2 * |(x,y)|) <= (|.x.| ^2) + (2 * (|.x.| * |.y.|)) by XREAL_1:7;

|.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) by A1, Th10;

then A3: |.(x + y).| ^2 <= ((|.x.| ^2) + ((2 * |.x.|) * |.y.|)) + (|.y.| ^2) by A2, XREAL_1:7;

0 <= |.(x + y).| ^2 by XREAL_1:63;

then sqrt (|.(x + y).| ^2) <= sqrt ((|.x.| + |.y.|) ^2) by A3, SQUARE_1:26;

then A4: |.(x + y).| <= sqrt ((|.x.| + |.y.|) ^2) by EUCLID:9, SQUARE_1:22;

( 0 <= |.x.| & 0 <= |.y.| ) by EUCLID:9;

then 0 + 0 <= |.x.| + |.y.| by XREAL_1:7;

hence |.(x + y).| <= |.x.| + |.y.| by A4, SQUARE_1:22; :: thesis: verum