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