theorem :: SERIES_5:28

for m, x, y, z being Real holds (m * x) + (z * y) <= (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2)))