let i be Integer; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) holds
p1 = p2
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) implies p1 = p2 )
( |.(euc2cpx p1).| = |.p1.| & |.(euc2cpx p2).| = |.p2.| ) by EUCLID_3:25;
hence ( |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) implies p1 = p2 ) by Th12, EUCLID_3:4; :: thesis: verum