let a, b, c, d be Complex; :: thesis: ((a - b) - c) / d = ((a / d) - (b / d)) - (c / d)
thus ((a - b) - c) / d = ((a - b) / d) - (c / d) by Th120
.= ((a / d) - (b / d)) - (c / d) by Th120 ; :: thesis: verum