let x be G_INTEG; :: thesis: ( Re x <> 0 & Im x <> 0 & Re x <> Im x & - (Re x) <> Im x implies not x *' is_associated_to x )
assume A1: ( Re x <> 0 & Im x <> 0 & Re x <> Im x & - (Re x) <> Im x ) ; :: thesis: not x *' is_associated_to x
assume x *' is_associated_to x ; :: thesis: contradiction
then consider d being G_INTEG such that
A2: ( d is g_int_unit & x = d * (x *') ) by Th40;
A3: x *' = (Re x) + ((- (Im x)) * <i>) ;

now :: thesis: contradiction

per cases ( d = 1 or d = - 1 or d = <i> or d = - <i> ) by A2, Th35;

suppose d = 1 ; :: thesis: contradiction

then Im x = - (Im x) by A2, A3, COMPLEX1:12;
hence contradiction by A1; :: thesis: verum

end;

suppose d = - 1 ; :: thesis: contradiction

then Re x = Re (- (x *')) by A2
.= - (Re (x *')) by COMPLEX1:17
.= - (Re x) by COMPLEX1:12, A3 ;
hence contradiction by A1; :: thesis: verum

end;

suppose d = <i> ; :: thesis: contradiction

then Im x = Im ((<i> * (Re x)) + (((- (Im x)) * <i>) * <i>)) by A2
.= Re x by COMPLEX1:12 ;
hence contradiction by A1; :: thesis: verum

end;

suppose d = - <i> ; :: thesis: contradiction

then Im x = Im ((<i> * (- (Re x))) + ((Im x) * (- 1r))) by A2
.= - (Re x) by COMPLEX1:12 ;
hence contradiction by A1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum