let a, b, c be Complex; :: thesis: ( b <> 0 implies (a / b) + c = (a + (b * c)) / b )
assume A1: b <> 0 ; :: thesis: (a / b) + c = (a + (b * c)) / b
(a / b) + c = (a / b) + (1 * c)
.= (a / b) + ((b * (b ")) * c) by A1, XCMPLX_0:def 7
.= (a / b) + ((b * c) * (b "))
.= (a / b) + ((c * b) / b) by XCMPLX_0:def 9
.= (a + (c * b)) / b by Th62 ;
hence (a / b) + c = (a + (b * c)) / b ; :: thesis: verum