theorem Th2: :: HERMITAN:2

for a being Complex st a <> 0c holds
( |.(((Re a) / |.a.|) + (((- (Im a)) / |.a.|) * <i>)).| = 1 & Re ((((Re a) / |.a.|) + (((- (Im a)) / |.a.|) * <i>)) * a) = |.a.| & Im ((((Re a) / |.a.|) + (((- (Im a)) / |.a.|) * <i>)) * a) = 0 )