let a, b be Complex; :: thesis: ( b <> 0 & b / a = - b implies a = - 1 )
assume that
A1: b <> 0 and
A2: b / a = - b ; :: thesis: a = - 1
a <> 0 by A1, A2, Th49;
then b = (- b) * a by A2, Lm3;
then b = - (b * a) ;
hence a = - 1 by A1, A2, Th181; :: thesis: verum