let x, y be ExtReal; :: thesis: |.(x * y).| = |.x.| * |.y.|
reconsider x = x, y = y as R_eal by XXREAL_0:def 1;

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

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

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

end;

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

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

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

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

end;

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

then A2: |.y.| = y by Def1;
|.x.| = x by A1, Def1;
hence |.(x * y).| = |.x.| * |.y.| by A2, Def1; :: thesis: verum

end;

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

then A4: |.y.| = - y by Def1;
|.x.| = x by A1, Def1;
then |.x.| * |.y.| = - (x * y) by A4, XXREAL_3:92;
hence |.(x * y).| = |.x.| * |.y.| by A1, A3, Def1; :: thesis: verum

end;

end;

end;

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

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

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

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

end;

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

then |.y.| = y by Def1;
then A7: |.x.| * |.y.| = (- x) * y by A5, Def1;
|.(x * y).| = - (x * y) by A5, A6, Def1;
hence |.(x * y).| = |.x.| * |.y.| by A7, XXREAL_3:92; :: thesis: verum

end;

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

then |.y.| = - y by Def1;
then |.x.| * |.y.| = (- x) * (- y) by A5, Def1;
then |.x.| * |.y.| = - (x * (- y)) by XXREAL_3:92
.= - (- (x * y)) by XXREAL_3:92 ;
hence |.(x * y).| = |.x.| * |.y.| by Def1; :: thesis: verum

end;

end;

end;

end;