let z be Complex; :: 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:44; :: 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;