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;
A5: |.x.| = +infty by A3, EXTREAL1:36;

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, Th17;
then |.(x / y).| = +infty by EXTREAL1:36;
hence |.(x / y).| = |.x.| / |.y.| by A4, A5, A6, A7, Th17; :: thesis: verum

end;

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

then |.y.| = - y by EXTREAL1:37;
then A9: |.y.| < +infty by A4, SUPINF_2:4, SUPINF_2:17;
A10: 0 < |.y.| by A2, Th52;
x / y = -infty by A3, A4, A8, Th18;
then |.(x / y).| = +infty by EXTREAL1:37, SUPINF_2:4;
hence |.(x / y).| = |.x.| / |.y.| by A5, A9, A10, Th17; :: 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;
A13: |.x.| = +infty by A11, EXTREAL1:37, SUPINF_2:4;

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, Th18;
then |.(x / y).| = +infty by EXTREAL1:37, SUPINF_2:4;
hence |.(x / y).| = |.x.| / |.y.| by A12, A13, A14, A15, Th17; :: thesis: verum

end;

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

then |.y.| = - y by EXTREAL1:37;
then A17: |.y.| < +infty by A12, SUPINF_2:4, SUPINF_2:17;
A18: 0 < |.y.| by A2, Th52;
x / y = +infty by A11, A12, A16, Th17;
then |.(x / y).| = +infty by EXTREAL1:36;
hence |.(x / y).| = |.x.| / |.y.| by A13, A17, A18, Th17; :: thesis: verum

end;

end;

end;

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

end;

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

then reconsider a = x as Real by XXREAL_0:14;
x is Real by A19, XXREAL_0:14;
then ( -infty < x & x < +infty ) by XXREAL_0:9, XXREAL_0:12;
then ( - +infty < x & x < +infty ) by EXTREAL1:4;
then A20: |.x.| < +infty by Th59;
A21: ( -infty < 0 & 0 <= |.x.| ) by Th51;

now

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

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

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

end;

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

then x / y = 0 by A19, EXTREAL1:33;
then A25: |.(x / y).| = 0 by EXTREAL1:def 3;
|.y.| = +infty by A24, EXTREAL1:37, SUPINF_2:4;
hence |.(x / y).| = |.x.| / |.y.| by A20, A21, A25, EXTREAL1:33; :: 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 A2, EXTREAL1:32;
then A26: |.(x / y).| = abs (a / b) by Th49;
A27: 0 <> |.y.| by A2, Th52;
( |.x.| = abs a & |.y.| = abs b ) by Th49;
then |.x.| / |.y.| = (abs a) / (abs b) by A27, 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;