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 A4: y < +infty by A1, XXREAL_0:9, XXREAL_0:14;
A5: -infty < y by A1, A3, XXREAL_0:12, XXREAL_0:14;

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

then A13: y < +infty by A1, XXREAL_0:9, XXREAL_0:14;
A14: -infty < y by A1, A12, XXREAL_0:12, XXREAL_0:14;

now

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

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

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

end;

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

then |.y.| = - y by EXTREAL1:37;
then A19: |.y.| < +infty by A14, XXREAL_3:5, XXREAL_3:40;
x / y = +infty by A12, A14, A18, XXREAL_3:95;
then A20: |.(x / y).| = +infty by EXTREAL1:36;
( 0 < |.y.| & |.x.| = +infty ) by A2, A12, Th52, EXTREAL1:37, XXREAL_3:5;
hence |.(x / y).| = |.x.| / |.y.| by A19, A20, 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 y = +infty ; :: thesis: |.(x / y).| = |.x.| / |.y.|

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

end;

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

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

end;

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

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

end;

end;

end;

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

end;

end;