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

assume A1: 0 <= x * y ; :: thesis: |.(x + y).| = |.x.| + |.y.|

assume A1: 0 <= x * y ; :: thesis: |.(x + y).| = |.x.| + |.y.|

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

end;

suppose A5:
0 < x * y
; :: thesis: |.(x + y).| = |.x.| + |.y.|

then A6:
( x <> 0 & y <> 0 )
;

end;