for F being non degenerated almost_left_invertible commutative Ring
for a, b, c, d being Element of F st b <> 0. F & d <> 0. F holds
(a / b) * (c / d) = (a * c) / (b * d)