:: deftheorem Def1 defines Arg COMPTRIG:def 1 :
for z being Complex
for b₂ being Real holds
( ( z <> 0 implies ( b₂ = Arg z iff ( z = (|.z.| * (cos b₂)) + ((|.z.| * (sin b₂)) * <i>) & 0 <= b₂ & b₂ < 2 * PI ) ) ) & ( not z <> 0 implies ( b₂ = Arg z iff b₂ = 0 ) ) );