let x, y be ExtReal; :: 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.|
reconsider y = y as R_eal by XXREAL_0:def 1;

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

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

A4: -infty < y by A1, A3, XXREAL_0:12, XXREAL_0:14;

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

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

then x / y = +infty by A3, A1, XXREAL_3:83;
then A6: |.(x / y).| = +infty by Def1;
|.y.| = y by A5, Def1;
hence |.(x / y).| = |.x.| / |.y.| by A3, A1, A5, A6, XXREAL_3:83; :: thesis: verum

end;

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

then |.y.| = - y by Def1;
then A8: |.y.| < +infty by A4, XXREAL_3:5, XXREAL_3:38;
x / y = -infty by A3, A1, A7, XXREAL_3:85;
then |.(x / y).| = +infty by Def1, XXREAL_3:5;
hence |.(x / y).| = |.x.| / |.y.| by A8, A2, A3, Th4, XXREAL_3:83; :: thesis: verum

end;

end;

end;

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

A10: -infty < y by A1, A9, XXREAL_0:12, XXREAL_0:14;

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

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

then A12: x / y = -infty by A9, A1, XXREAL_3:86;
A13: |.x.| = +infty by A9, Def1, XXREAL_3:5;
|.y.| = y by A11, Def1;
hence |.(x / y).| = |.x.| / |.y.| by A9, A1, A11, A12, A13, XXREAL_3:83; :: thesis: verum

end;

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

then |.y.| = - y by Def1;
then A15: |.y.| < +infty by A10, XXREAL_3:5, XXREAL_3:38;
A16: x / y = +infty by A9, A1, A14, XXREAL_3:84;
( 0 < |.y.| & |.x.| = +infty ) by A2, A9, Th4, Def1, XXREAL_3:5;
hence |.(x / y).| = |.x.| / |.y.| by A15, A16, XXREAL_3:83; :: thesis: verum

end;

end;

end;

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

then reconsider a = x as Element of REAL by XXREAL_0:14;

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 Def1;
hence |.(x / y).| = |.x.| / |.y.| ; :: thesis: verum

end;

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

then ( |.(x / y).| = 0 & |.y.| = +infty ) by Def1, 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 Element of REAL by XXREAL_0:14;
( |.x.| = |.a.| & |.y.| = |.b.| ) by Th1;
then A17: |.x.| / |.y.| = |.a.| / |.b.| by Th2;
x / y = a / b by Th2;
then |.(x / y).| = |.(a / b).| by Th1;
hence |.(x / y).| = |.x.| / |.y.| by A17, COMPLEX1:67; :: thesis: verum

end;

end;

end;

end;