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:24, COMPLEX2:34;
( cpx2euc (|.(euc2cpx p).| + (0 * <i> )) = |[|.(euc2cpx p).|,0 ]| & |.(euc2cpx p).| = |.p.| ) by Th9, Th31;
hence ( p = |[|.p.|,0 ]| & p `2 = 0 ) by A1, Th2, COMPLEX1:28; :: thesis: verum