let a, b, c be Complex; :: 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