let a be Complex; :: thesis: ( a <> 0 & a = a " & not a = 1 implies a = - 1 )
assume A1: a <> 0 ; :: thesis: ( not a = a " or a = 1 or a = - 1 )
assume a = a " ; :: thesis: ( a = 1 or a = - 1 )
then a * a = 1 by A1, XCMPLX_0:def 7;
hence ( a = 1 or a = - 1 ) by Th182; :: thesis: verum