let z be Element of F_Complex; :: thesis: ( z <> 0. F_Complex implies ( |.[**((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 ) )
reconsider b = z as Element of COMPLEX by COMPLFLD:def 1;
set a = [**((Re z) / |.z.|),((- (Im z)) / |.z.|)**];
set a1 = ((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>);
A1: [**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z = (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * b ;
assume z <> 0. F_Complex ; :: 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 )
hence ( |.[**((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 A1, Th2, COMPLFLD:7; :: thesis: verum