for a being Element of F_Complex st a <> 0. F_Complex holds
( |.[**((Re a) / |.a.|),((- (Im a)) / |.a.|)**].| = 1 & Re ([**((Re a) / |.a.|),((- (Im a)) / |.a.|)**] * a) = |.a.| & Im ([**((Re a) / |.a.|),((- (Im a)) / |.a.|)**] * a) = 0 ) by Th2, COMPLFLD:7;