let a be Complex; :: 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 COMPTRIG:62;
then A1: ( Re a = |.a.| * (cos (Arg a)) & Im a = |.a.| * (sin (Arg a)) ) by COMPLEX1:12;
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:45, XCMPLX_1:89; :: thesis: verum