let a, c, b be complex number ; :: thesis: (a / c) - (b / c) = (a - b) / c
thus (a / c) - (b / c) = (a / c) + (- (b / c))
.= (a / c) + ((- b) / c) by Lm18
.= (a + (- b)) / c by Th63
.= (a - b) / c ; :: thesis: verum