let x, y be ExtReal; :: thesis: ( 0 <= x * y implies |.(x + y).| = |.x.| + |.y.| )
assume A1: 0 <= x * y ; :: thesis: |.(x + y).| = |.x.| + |.y.|

per cases ( ( ( 0 <= x or 0 < x ) & ( 0 <= y or 0 < y ) ) or ( ( x <= 0 or x < 0 ) & ( y <= 0 or y < 0 ) ) ) by A1;

suppose ( ( 0 <= x or 0 < x ) & ( 0 <= y or 0 < y ) ) ; :: thesis: |.(x + y).| = |.x.| + |.y.|

then ( |.x.| = x & |.y.| = y ) by Def1;
hence |.(x + y).| = |.x.| + |.y.| by Def1; :: thesis: verum

end;

suppose A2: ( ( x <= 0 or x < 0 ) & ( y <= 0 or y < 0 ) ) ; :: thesis: |.(x + y).| = |.x.| + |.y.|

then A3: |.(x + y).| = - (x + y) by Th7
.= (- x) - y by XXREAL_3:25 ;
|.x.| = - x by A2, Th7;
hence |.(x + y).| = |.x.| + |.y.| by A2, A3, Th7; :: thesis: verum

end;

end;