let x, y be ExtReal; :: thesis: |.(x * y).| = |.x.| * |.y.|

reconsider x = x, y = y as R_eal by XXREAL_0:def 1;

reconsider x = x, y = y as R_eal by XXREAL_0:def 1;

per cases
( x = 0 or 0 < x or x < 0 )
;

end;

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

end;

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

end;

per cases
( y = 0 or 0 < y or y < 0 )
;

end;