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 * y = 0 & |.x.| = 0 ) by EXTREAL1:def 3;
then ( |.(x * y).| = 0 & |.x.| * |.y.| = 0 ) by EXTREAL1:def 3;
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 ( x * y = 0 & |.y.| = 0 ) by EXTREAL1:def 3;
then ( |.(x * y).| = 0 & |.x.| * |.y.| = 0 ) by EXTREAL1:def 3;
hence |.(x * y).| = |.x.| * |.y.| ; :: thesis: verum

end;

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

then ( 0 <= x * y & |.x.| = x & |.y.| = y ) by A1, EXTREAL1:def 3;
hence |.(x * y).| = |.x.| * |.y.| by EXTREAL1:def 3; :: thesis: verum

end;

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

then ( |.x.| = x & |.y.| = - y ) by A1, EXTREAL1:def 3;
then |.x.| * |.y.| = - (x * y) by XXREAL_3:103;
hence |.(x * y).| = |.x.| * |.y.| by A1, A2, EXTREAL1:def 3; :: thesis: verum

end;

end;

end;

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

end;

suppose A4: 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 ( x * y = 0 & |.y.| = 0 ) by EXTREAL1:def 3;
then ( |.(x * y).| = 0 & |.x.| * |.y.| = 0 ) by EXTREAL1:def 3;
hence |.(x * y).| = |.x.| * |.y.| ; :: thesis: verum

end;

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

then ( not 0 <= x * y & |.y.| = y ) by A4, EXTREAL1:def 3;
then ( |.(x * y).| = - (x * y) & |.x.| * |.y.| = (- x) * y ) by A4, EXTREAL1:def 3;
hence |.(x * y).| = |.x.| * |.y.| by XXREAL_3:103; :: thesis: verum

end;

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

then ( 0 <= x * y & |.y.| = - y ) by A4, EXTREAL1:def 3;
then ( |.(x * y).| = x * y & |.x.| * |.y.| = (- x) * (- y) ) by A4, EXTREAL1:def 3;
then |.x.| * |.y.| = - (x * (- y)) by XXREAL_3:103
.= - (- (x * y)) by XXREAL_3:103 ;
hence |.(x * y).| = |.x.| * |.y.| by S, A4, EXTREAL1:def 3; :: thesis: verum

end;

end;

end;

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

end;

end;