let a, b, c, d be Complex; ( b <> 0 & d <> 0 implies (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d) )
assume A1:
b <> 0
; ( not d <> 0 or (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d) )
assume A2:
d <> 0
; (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d)
thus (a / b) - (c / d) =
(a / b) + (- (c / d))
.=
(a / b) + ((- c) / d)
by Lm17
.=
((a * d) + ((- c) * b)) / (b * d)
by A1, A2, Th116
.=
((a * d) - (c * b)) / (b * d)
; verum