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 A3: ( ( x <= 0 or x < 0 ) & ( y <= 0 or y < 0 ) ) ; :: thesis: |.(x + y).| = |.x.| + |.y.|

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

end;

end;