let x, y be R_eal; :: 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 A2: ( ( 0 <= x or 0 < x ) & ( 0 <= y or 0 < y ) ) ; :: thesis: |.(x + y).| = |.x.| + |.y.|

then ( |.x.| = x & |.y.| = y ) by EXTREAL1:def 3;
hence |.(x + y).| = |.x.| + |.y.| by A2, EXTREAL1:def 3; :: thesis: verum

end;

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

then A5: ( |.x.| = - x & |.y.| = - y ) by Th55;
|.(x + y).| = - (x + y) by A4, Th55
.= (- x) - y by XXREAL_3:26 ;
hence |.(x + y).| = |.x.| + |.y.| by A5; :: thesis: verum

end;

end;