let a, b be Complex; :: thesis: ( b <> 0 & a * b = - b implies a = - 1 )
assume that
A1: b <> 0 and
A2: a * b = - b ; :: thesis: a = - 1
a * (b * (b ")) = (- b) * (b ") by A2, 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