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