let a, c, b be complex number ; :: thesis: (a / c) + (b / c) = (a + b) / c
thus (a / c) + (b / c) = (a * (c " )) + (b / c) by XCMPLX_0:def 9
.= (a * (c " )) + (b * (c " )) by XCMPLX_0:def 9
.= (a + b) * (c " )
.= (a + b) / c by XCMPLX_0:def 9 ; :: thesis: verum