let x, y be R_eal; :: thesis: ( ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) & y <> 0 implies |.(x / y).| = |.x.| / |.y.| )
assume that
A1: ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) and
A2: y <> 0 ; :: thesis: |.(x / y).| = |.x.| / |.y.|

per cases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;

suppose A3: x = +infty ; :: thesis: |.(x / y).| = |.x.| / |.y.|

then y is Real by A1, XXREAL_0:14;
then A4: ( -infty < y & y < +infty ) by XXREAL_0:9, XXREAL_0:12;

now

per cases ( 0 < y or y < 0 ) by A2;

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

then A7: |.y.| = y by EXTREAL1:36;
x / y = +infty by A3, A4, A6, XXREAL_3:94;
then X: |.(x / y).| = +infty by EXTREAL1:36;
|.x.| = +infty by A3, EXTREAL1:36;
hence |.(x / y).| = |.x.| / |.y.| by A4, A6, A7, X, XXREAL_3:94; :: thesis: verum

end;

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

then |.y.| = - y by EXTREAL1:37;
then A9: |.y.| < +infty by A4, XXREAL_3:5, XXREAL_3:40;
A10: 0 < |.y.| by A2, Th52;
x / y = -infty by A3, A4, A8, XXREAL_3:96;
then X: |.(x / y).| = +infty by EXTREAL1:37, XXREAL_3:5;
|.x.| = +infty by A3, EXTREAL1:36;
hence |.(x / y).| = |.x.| / |.y.| by A9, A10, X, XXREAL_3:94; :: thesis: verum

end;

end;

end;

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

end;

suppose A11: x = -infty ; :: thesis: |.(x / y).| = |.x.| / |.y.|

then y is Real by A1, XXREAL_0:14;
then A12: ( -infty < y & y < +infty ) by XXREAL_0:9, XXREAL_0:12;

now

per cases ( 0 < y or y < 0 ) by A2;

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

then A15: |.y.| = y by EXTREAL1:36;
x / y = -infty by A11, A12, A14, XXREAL_3:97;
then X: |.(x / y).| = +infty by EXTREAL1:37, XXREAL_3:5;
|.x.| = +infty by A11, EXTREAL1:37, XXREAL_3:5;
hence |.(x / y).| = |.x.| / |.y.| by A12, A14, A15, X, XXREAL_3:94; :: thesis: verum

end;

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

then |.y.| = - y by EXTREAL1:37;
then A17: |.y.| < +infty by A12, XXREAL_3:5, XXREAL_3:40;
A18: 0 < |.y.| by A2, Th52;
x / y = +infty by A11, A12, A16, XXREAL_3:95;
then X: |.(x / y).| = +infty by EXTREAL1:36;
|.x.| = +infty by A11, EXTREAL1:37, XXREAL_3:5;
hence |.(x / y).| = |.x.| / |.y.| by X, A17, A18, XXREAL_3:94; :: thesis: verum

end;

end;

end;

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

end;

suppose ( x <> +infty & x <> -infty ) ; :: thesis: |.(x / y).| = |.x.| / |.y.|

then reconsider a = x as Real by XXREAL_0:14;

now

per cases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ;

suppose A22: y = +infty ; :: thesis: |.(x / y).| = |.x.| / |.y.|

then A23: |.(x / y).| = 0 by EXTREAL1:def 3;
|.y.| = +infty by A22, EXTREAL1:36;
hence |.(x / y).| = |.x.| / |.y.| by A23; :: thesis: verum

end;

suppose A24: y = -infty ; :: thesis: |.(x / y).| = |.x.| / |.y.|

then A25: |.(x / y).| = 0 by EXTREAL1:def 3;
|.y.| = +infty by A24, EXTREAL1:37, XXREAL_3:5;
hence |.(x / y).| = |.x.| / |.y.| by A25; :: thesis: verum

end;

suppose ( y <> +infty & y <> -infty ) ; :: thesis: |.(x / y).| = |.x.| / |.y.|

then reconsider b = y as Real by XXREAL_0:14;
x / y = a / b by EXTREAL1:32;
then A26: |.(x / y).| = abs (a / b) by Th49;
( |.x.| = abs a & |.y.| = abs b ) by Th49;
then |.x.| / |.y.| = (abs a) / (abs b) by EXTREAL1:32;
hence |.(x / y).| = |.x.| / |.y.| by A26, COMPLEX1:153; :: thesis: verum

end;

end;

end;

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

end;

end;