let x be Real; :: thesis: ( x > 0 implies Arg (x * <i> ) = PI / 2 )
assume A1: x > 0 ; :: thesis: Arg (x * <i> ) = PI / 2
A3: ( 0 <= Arg (0 + (x * <i> )) & Arg (0 + (x * <i> )) < 2 * PI ) by Th52;
A4: 0 + (x * <i> ) <> 0 by A1;
then A5: |.(0 + (x * <i> )).| <> 0 by COMPLEX1:131;
A6: 0 + (x * <i> ) = (|.(0 + (x * <i> )).| * (cos (Arg (0 + (x * <i> ))))) + ((|.(0 + (x * <i> )).| * (sin (Arg (0 + (x * <i> ))))) * <i> ) by A4, Def1;
then cos (Arg (0 + (x * <i> ))) = 0 by A5, COMPLEX1:163;
then ( Arg (0 + (x * <i> )) = PI / 2 or |.(0 + (x * <i> )).| * (- 1) = x ) by A3, A6, Th34, SIN_COS:82;
then ( Arg (0 + (x * <i> )) = PI / 2 or |.(0 + (x * <i> )).| < 0 ) by A1;
hence Arg (x * <i> ) = PI / 2 by COMPLEX1:132; :: thesis: verum