let p be real number ; :: thesis: for z being complex number st p > 0 holds
( Re (z / (p * <i> )) = (Im z) / p & Im (z / (p * <i> )) = - ((Re z) / p) & |.(z / p).| = |.z.| / p )
let z be complex number ; :: thesis: ( p > 0 implies ( Re (z / (p * <i> )) = (Im z) / p & Im (z / (p * <i> )) = - ((Re z) / p) & |.(z / p).| = |.z.| / p ) )
assume A1: p > 0 ; :: thesis: ( Re (z / (p * <i> )) = (Im z) / p & Im (z / (p * <i> )) = - ((Re z) / p) & |.(z / p).| = |.z.| / p )
A2: ( Re (0 + (p * <i> )) = 0 & Im (0 + (p * <i> )) = p & Re (p + (0 * <i> )) = p & Im (p + (0 * <i> )) = 0 ) by COMPLEX1:28;
then A3: z / (p * <i> ) = ((((Re z) * 0 ) + ((Im z) * p)) / ((0 ^2 ) + (p ^2 ))) + ((((0 * (Im z)) - ((Re z) * p)) / ((0 ^2 ) + (p ^2 ))) * <i> ) by COMPLEX1:def 14
.= (((Im z) * p) / (p * p)) + ((((- (Re z)) * p) / (p * p)) * <i> )
.= (((Im z) * p) / (p * p)) + (((- (Re z)) / p) * <i> ) by A1, XCMPLX_1:92
.= ((Im z) / p) + ((- ((Re z) / p)) * <i> ) by A1, XCMPLX_1:92 ;
|.(z / p).| = |.z.| / |.p.| by COMPLEX1:153
.= |.z.| / (sqrt (p ^2 )) by A2 ;
hence ( Re (z / (p * <i> )) = (Im z) / p & Im (z / (p * <i> )) = - ((Re z) / p) & |.(z / p).| = |.z.| / p ) by A1, A3, COMPLEX1:28, SQUARE_1:89; :: thesis: verum