let a, b, c, d be Complex; :: thesis: ( b <> 0 & a / b = c / d implies a = (b * c) / d )
assume that
A1: b <> 0 and
A2: a / b = c / d ; :: thesis: a = (b * c) / d
thus a = b * (a / b) by A1, XCMPLX_1:87
.= (b * c) / d by A2, XCMPLX_1:74 ; :: thesis: verum