theorem :: EXTREAL1:28

for x, y being ExtReal st ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) & y <> 0 holds
|.(x / y).| = |.x.| / |.y.|