theorem :: ABSVALUE:11

for x, y being Real st 0 <= x * y holds
|.(x + y).| = |.x.| + |.y.|