let p be Point of (TOP-REAL 2); :: thesis: ( Arg p = 0 implies ( p = |[|.p.|,0]| & p `2 = 0 ) )
assume Arg p = 0 ; :: thesis: ( p = |[|.p.|,0]| & p `2 = 0 )
then A1: ( euc2cpx p = |.(euc2cpx p).| + (0 * <i>) & Im (euc2cpx p) = 0 ) by COMPLEX2:15, COMPLEX2:21;
( cpx2euc (|.(euc2cpx p).| + (0 * <i>)) = |[|.(euc2cpx p).|,0]| & |.(euc2cpx p).| = |.p.| ) by Th5, Th25;
hence ( p = |[|.p.|,0]| & p `2 = 0 ) by A1, Th2, COMPLEX1:12; :: thesis: verum