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

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 EXTREAL1:def 1;
hence |.(x * y).| = |.x.| * |.y.| ; :: thesis: verum

end;

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

now

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 EXTREAL1:def 1;
hence |.(x * y).| = |.x.| * |.y.| ; :: thesis: verum

end;

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

then A3: |.y.| = y by EXTREAL1:def 1;
|.x.| = x by A1, EXTREAL1:def 1;
hence |.(x * y).| = |.x.| * |.y.| by A1, A2, A3, EXTREAL1:def 1; :: thesis: verum

end;

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

then A5: |.y.| = - y by EXTREAL1:def 1;
|.x.| = x by A1, EXTREAL1:def 1;
then |.x.| * |.y.| = - (x * y) by A5, XXREAL_3:92;
hence |.(x * y).| = |.x.| * |.y.| by A1, A4, EXTREAL1:def 1; :: thesis: verum

end;

end;

end;

hence |.(x * y).| = |.x.| * |.y.| ; :: thesis: verum

end;

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

now

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 EXTREAL1:def 1;
hence |.(x * y).| = |.x.| * |.y.| ; :: thesis: verum

end;

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

then |.y.| = y by EXTREAL1:def 1;
then A8: |.x.| * |.y.| = (- x) * y by A6, EXTREAL1:def 1;
|.(x * y).| = - (x * y) by A6, A7, EXTREAL1:def 1;
hence |.(x * y).| = |.x.| * |.y.| by A8, XXREAL_3:92; :: thesis: verum

end;

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

then |.y.| = - y by EXTREAL1:def 1;
then |.x.| * |.y.| = (- x) * (- y) by A6, EXTREAL1:def 1;
then |.x.| * |.y.| = - (x * (- y)) by XXREAL_3:92
.= - (- (x * y)) by XXREAL_3:92 ;
hence |.(x * y).| = |.x.| * |.y.| by A6, A9, EXTREAL1:def 1; :: thesis: verum

end;

end;

end;

hence |.(x * y).| = |.x.| * |.y.| ; :: thesis: verum

end;

end;