let a be complex number ; :: thesis: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>)

per cases ( a <> 0 or a = 0c ) ;

suppose a <> 0 ; :: thesis: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>)

hence a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) by COMPTRIG:def 1; :: thesis: verum

end;

suppose a = 0c ; :: thesis: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>)

hence a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) by COMPLEX1:44; :: thesis: verum

end;

end;