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