theorem :: COMPTRIG:62

for z being Complex holds z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i>)