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 ) )

( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )

( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 ) by A1, COMPLEX1:46; :: thesis: verum

( |.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

( 0 < |.z.| implies ex a being Element of F_Complex st
assume A2:
|.z.| = 0
; :: thesis: ex a being Element of F_Complex st

( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )

take a = 1. F_Complex; :: thesis: ( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )

thus |.a.| = 1 by COMPLFLD:60; :: thesis: ( Re (a * z) = |.z.| & Im (a * z) = 0 )

z = 0. F_Complex by A2, COMPLFLD:58

.= 0 by COMPLFLD:def 1 ;

hence ( Re (a * z) = |.z.| & Im (a * z) = 0 ) by A2, Lm1, COMPLEX1:12; :: thesis: verum

end;( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )

take a = 1. F_Complex; :: thesis: ( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )

thus |.a.| = 1 by COMPLFLD:60; :: thesis: ( Re (a * z) = |.z.| & Im (a * z) = 0 )

z = 0. F_Complex by A2, COMPLFLD:58

.= 0 by COMPLFLD:def 1 ;

hence ( Re (a * z) = |.z.| & Im (a * z) = 0 ) by A2, Lm1, COMPLEX1:12; :: thesis: verum

( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )

proof

hence
ex b being Element of F_Complex st
assume A3:
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 A3, Th7, COMPLFLD:57; :: thesis: verum

end;( |.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 A3, Th7, COMPLFLD:57; :: thesis: verum

( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 ) by A1, COMPLEX1:46; :: thesis: verum