let a, b be complex number ; :: thesis: (a / (2 * b)) + (a / (2 * b)) = a / b
thus (a / (2 * b)) + (a / (2 * b)) = (a + a) / (2 * b) by Th63
.= (2 * a) / (2 * b)
.= a / b by Lm11 ; :: thesis: verum