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