let F be non degenerated almost_left_invertible commutative Ring; :: thesis: 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)
let a, b, c, d be Element of F; :: thesis: ( b <> 0. F & d <> 0. F implies (a / b) * (c / d) = (a * c) / (b * d) )
assume A1: ( b <> 0. F & d <> 0. F ) ; :: thesis: (a / b) * (c / d) = (a * c) / (b * d)
(a / b) * (c / d) = a * ((b ") * (c * (d "))) by GROUP_1:def 3
.= a * (((b ") * (d ")) * c) by GROUP_1:def 3
.= (a * c) * ((b ") * (d ")) by GROUP_1:def 3
.= (a * c) / (d * b) by A1, GCD_1:49 ;
hence (a / b) * (c / d) = (a * c) / (b * d) ; :: thesis: verum