let z be Element of COMPLEX ; :: thesis: ex b being Element of COMPLEX st
( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 )
set r = |.z.|;
A1: ( |.z.| = 0 implies ex a being Element of COMPLEX st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )

proof

assume A2: |.z.| = 0 ; :: thesis: ex a being Element of COMPLEX st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
take 1r ; :: thesis: ( |.1r .| = 1 & Re (1r * z) = |.z.| & Im (1r * z) = 0 )
thus ( |.1r .| = 1 & Re (1r * z) = |.z.| & Im (1r * z) = 0 ) by A2, COMPLEX1:12, COMPLEX1:131, COMPLEX1:134; :: thesis: verum

end;

( 0 < |.z.| implies ex a being Element of COMPLEX st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )

proof

assume A3: 0 < |.z.| ; :: thesis: ex a being Element of COMPLEX st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
take ((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i> ) ; :: thesis: ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i> )).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i> )) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i> )) * z) = 0 )
thus ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i> )).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i> )) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i> )) * z) = 0 ) by A3, Th2, COMPLEX1:130; :: thesis: verum

end;

hence ex b being Element of COMPLEX st
( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 ) by A1, COMPLEX1:132; :: thesis: verum