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