theorem Th2: :: HAHNBAN1:3

for z being Element of COMPLEX holds |.z.| + (0 * <i>) = ((z *') / (|.z.| + (0 * <i>))) * z