let b, a be complex number ; :: thesis: ( b <> 0 implies a = (a * b) / b )
assume A1: b <> 0 ; :: thesis: a = (a * b) / b
a = a * 1 ;
then a = a * (b / b) by A1, Lm5;
then a = a * (b * (b " )) by XCMPLX_0:def 9;
then a = (a * b) * (b " ) ;
hence a = (a * b) / b by XCMPLX_0:def 9; :: thesis: verum