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