let i be Integer; :: thesis: for c1, c2 being Complex st |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) holds
c1 = c2
let c1, c2 be Complex; :: thesis: ( |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) implies c1 = c2 )
assume A1: ( |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) ) ; :: thesis: c1 = c2
A2: ( cos (Arg c2) = cos ((Arg c2) + ((2 * PI) * i)) & sin (Arg c2) = sin ((Arg c2) + ((2 * PI) * i)) ) by COMPLEX2:8, COMPLEX2:9;
( c1 = (|.c1.| * (cos (Arg c1))) + ((|.c1.| * (sin (Arg c1))) * <i>) & c2 = (|.c2.| * (cos (Arg c2))) + ((|.c2.| * (sin (Arg c2))) * <i>) ) by COMPTRIG:62;
hence c1 = c2 by A1, A2; :: thesis: verum