let a, b, c, d be Complex; :: thesis: ( b <> 0 & d <> 0 implies (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) )
assume A1: b <> 0 ; :: thesis: ( not d <> 0 or (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) )
assume d <> 0 ; :: thesis: (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)
hence (a / b) + (c / d) = ((a * d) / (b * d)) + (c / d) by Lm10
.= ((a * d) / (b * d)) + ((c * b) / (b * d)) by A1, Lm10
.= ((a * d) + (c * b)) / (b * d) by Th62 ;
:: thesis: verum