theorem :: COMPLEX1:78

for a, b being Real holds sqrt ((a ^2) + (b ^2)) <= |.a.| + |.b.|