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 " )) = (- b) * (b " ) by Th4;
then a * 1 = (- b) * (b " ) by A1, XCMPLX_0:def 7;
hence a = - (b * (b " ))
.= - 1 by A1, XCMPLX_0:def 7 ;
:: thesis: verum