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

proof

assume A2: |.z.| = 0 ; :: thesis: ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
then A3: z = 0. F_Complex by COMPLFLD:94
.= 0 by COMPLFLD:def 1 ;
take a = 1. F_Complex ; :: thesis: ( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
thus |.a.| = 1 by COMPLFLD:97; :: thesis: ( Re (a * z) = |.z.| & Im (a * z) = 0 )
thus ( Re (a * z) = |.z.| & Im (a * z) = 0 ) by A2, A3, Lm1, COMPLEX1:28; :: thesis: verum

end;

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

proof

assume A4: 0 < |.z.| ; :: thesis: ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
take [**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] ; :: thesis: ( |.[**((Re z) / |.z.|),((- (Im z)) / |.z.|)**].| = 1 & Re ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = |.z.| & Im ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = 0 )
thus ( |.[**((Re z) / |.z.|),((- (Im z)) / |.z.|)**].| = 1 & Re ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = |.z.| & Im ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = 0 ) by A4, Th8, COMPLFLD:93; :: thesis: verum

end;

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