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

per cases ( z = 0 or z <> 0 ) ;

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

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

end;

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

hence z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i> ) by Def1; :: thesis: verum

end;

end;