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)| <= abs |(x,y)| & abs |(x,y)| <= |.x.| * |.y.| ) by Th37, ABSVALUE:11;
then |(x,y)| <= |.x.| * |.y.| by XXREAL_0:2;
then 2 * |(x,y)| <= 2 * (|.x.| * |.y.|) by XREAL_1:66;
then A2: (|.x.| ^2 ) + (2 * |(x,y)|) <= (|.x.| ^2 ) + (2 * (|.x.| * |.y.|)) by XREAL_1:9;
|.(x + y).| ^2 = ((|.x.| ^2 ) + (2 * |(y,x)|)) + (|.y.| ^2 ) by A1, Th33;
then A3: |.(x + y).| ^2 <= ((|.x.| ^2 ) + ((2 * |.x.|) * |.y.|)) + (|.y.| ^2 ) by A2, XREAL_1:9;
0 <= |.(x + y).| ^2 by XREAL_1:65;
then sqrt (|.(x + y).| ^2 ) <= sqrt ((|.x.| + |.y.|) ^2 ) by A3, SQUARE_1:94;
then A4: |.(x + y).| <= sqrt ((|.x.| + |.y.|) ^2 ) by Th14, SQUARE_1:89;
( 0 <= |.x.| & 0 <= |.y.| ) by Th14;
then 0 + 0 <= |.x.| + |.y.| by XREAL_1:9;
hence |.(x + y).| <= |.x.| + |.y.| by A4, SQUARE_1:89; :: thesis: verum