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