let m, x, u, y, w, z be real number ; :: thesis: (((m * x) + (u * y)) + (w * z)) ^2 <= (((m ^2 ) + (u ^2 )) + (w ^2 )) * (((x ^2 ) + (y ^2 )) + (z ^2 ))
((m ^2 ) * (z ^2 )) + ((w ^2 ) * (x ^2 )) = ((m * z) ^2 ) + ((w * x) ^2 ) ;
then A1: ((m ^2 ) * (z ^2 )) + ((w ^2 ) * (x ^2 )) >= (2 * (m * z)) * (w * x) by SERIES_3:6;
((u ^2 ) * (z ^2 )) + ((w ^2 ) * (y ^2 )) = ((u * z) ^2 ) + ((w * y) ^2 ) ;
then A2: ((u ^2 ) * (z ^2 )) + ((w ^2 ) * (y ^2 )) >= (2 * (u * z)) * (w * y) by SERIES_3:6;
((m * y) ^2 ) + ((u * x) ^2 ) >= (2 * (m * y)) * (u * x) by SERIES_3:6;
then (((m ^2 ) * (y ^2 )) + ((u ^2 ) * (x ^2 ))) + (((m ^2 ) * (z ^2 )) + ((w ^2 ) * (x ^2 ))) >= ((((2 * m) * y) * u) * x) + ((((2 * m) * z) * w) * x) by A1, XREAL_1:9;
then (((((m ^2 ) * (y ^2 )) + ((u ^2 ) * (x ^2 ))) + ((m ^2 ) * (z ^2 ))) + ((w ^2 ) * (x ^2 ))) + (((u ^2 ) * (z ^2 )) + ((w ^2 ) * (y ^2 ))) >= (((((2 * m) * y) * u) * x) + ((((2 * m) * z) * w) * x)) + ((((2 * u) * z) * w) * y) by A2, XREAL_1:9;
then (((((((m ^2 ) * (y ^2 )) + ((u ^2 ) * (x ^2 ))) + ((m ^2 ) * (z ^2 ))) + ((w ^2 ) * (x ^2 ))) + ((u ^2 ) * (z ^2 ))) + ((w ^2 ) * (y ^2 ))) + ((((m * x) ^2 ) + ((u * y) ^2 )) + ((w * z) ^2 )) >= ((((((2 * m) * y) * u) * x) + ((((2 * m) * z) * w) * x)) + ((((2 * u) * z) * w) * y)) + ((((m * x) ^2 ) + ((u * y) ^2 )) + ((w * z) ^2 )) by XREAL_1:8;
hence (((m * x) + (u * y)) + (w * z)) ^2 <= (((m ^2 ) + (u ^2 )) + (w ^2 )) * (((x ^2 ) + (y ^2 )) + (z ^2 )) ; :: thesis: verum