let x be Real; :: thesis: ( x > 0 implies Arg (x * <i>) = PI / 2 )
A1: ( 0 <= Arg (0 + (x * <i>)) & Arg (0 + (x * <i>)) < 2 * PI ) by Th34;
assume A2: x > 0 ; :: thesis: Arg (x * <i>) = PI / 2
then A3: 0 + (x * <i>) <> 0 ;
then A4: 0 + (x * <i>) = (|.(0 + (x * <i>)).| * (cos (Arg (0 + (x * <i>))))) + ((|.(0 + (x * <i>)).| * (sin (Arg (0 + (x * <i>))))) * <i>) by Def1;
|.(0 + (x * <i>)).| <> 0 by A3, COMPLEX1:45;
then cos (Arg (0 + (x * <i>))) = 0 by A4, COMPLEX1:77;
then ( Arg (0 + (x * <i>)) = PI / 2 or |.(0 + (x * <i>)).| * (- 1) = x ) by A1, A4, Th18, SIN_COS:77;
then ( Arg (0 + (x * <i>)) = PI / 2 or |.(0 + (x * <i>)).| < 0 ) by A2;
hence Arg (x * <i>) = PI / 2 by COMPLEX1:46; :: thesis: verum