let m, u, w, x, y, z be Real; (((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:7;
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:7;
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:6;
hence
(((m * x) + (u * y)) + (w * z)) ^2 <= (((m ^2) + (u ^2)) + (w ^2)) * (((x ^2) + (y ^2)) + (z ^2))
; verum