let a be complex number ; :: thesis: ( a <> 0 implies ( cos (Arg a) = (Re a) / |.a.| & sin (Arg a) = (Im a) / |.a.| ) )
a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i> ) by Th19;
then A1: ( Re a = |.a.| * (cos (Arg a)) & Im a = |.a.| * (sin (Arg a)) ) by COMPLEX1:28;
assume a <> 0 ; :: thesis: ( cos (Arg a) = (Re a) / |.a.| & sin (Arg a) = (Im a) / |.a.| )
hence ( cos (Arg a) = (Re a) / |.a.| & sin (Arg a) = (Im a) / |.a.| ) by A1, COMPLEX1:131, XCMPLX_1:90; :: thesis: verum