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:130; :: thesis: verum

end;

end;