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 * d) + (c * b)) / (b * d)
let a, b, c, d be Element of F; :: thesis: ( b <> 0. F & d <> 0. F implies (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) )
assume that
A1: b <> 0. F and
A2: d <> 0. F ; :: thesis: (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)
((a * d) + (c * b)) / (b * d) = ((a * d) + (c * b)) * ((b ") * (d ")) by A1, A2, GCD_1:49
.= (((a * d) + (c * b)) * (b ")) * (d ") by GROUP_1:def 3
.= (((a * d) * (b ")) + ((c * b) * (b "))) * (d ") by VECTSP_1:def 3
.= (((a * d) * (b ")) + (c * (b * (b ")))) * (d ") by GROUP_1:def 3
.= (((a * d) * (b ")) + (c * (1. F))) * (d ") by A1, VECTSP_1:def 10
.= (((a * d) * (b ")) + c) * (d ")
.= (((a * d) * (b ")) * (d ")) + (c * (d ")) by VECTSP_1:def 3
.= ((b ") * ((a * d) * (d "))) + (c * (d ")) by GROUP_1:def 3
.= ((b ") * (a * (d * (d ")))) + (c * (d ")) by GROUP_1:def 3
.= ((b ") * (a * (1. F))) + (c * (d ")) by A2, VECTSP_1:def 10
.= ((b ") * a) + (c * (d ")) ;
hence (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) ; :: thesis: verum