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 ) )
assume A1: 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 )
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> );
[**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z = (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i> )) * b ;
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:9; :: thesis: verum