let a, b be Complex; :: thesis: ( b <> 0 implies a = (a * b) / b )
A1: a = a * 1 ;
assume b <> 0 ; :: thesis: a = (a * b) / b
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