let p be Real; :: thesis: for z being complex number holds
( Re ((p * <i> ) * z) = - (p * (Im z)) & Im ((p * <i> ) * z) = p * (Re z) & Re (p * z) = p * (Re z) & Im (p * z) = p * (Im z) )
let z be complex number ; :: thesis: ( Re ((p * <i> ) * z) = - (p * (Im z)) & Im ((p * <i> ) * z) = p * (Re z) & Re (p * z) = p * (Re z) & Im (p * z) = p * (Im z) )
A1: (p * <i> ) * z = (p * <i> ) * ((Re z) + ((Im z) * <i> )) by COMPLEX1:29
.= (- (p * (Im z))) + ((p * (Re z)) * <i> ) ;
p * z = p * ((Re z) + ((Im z) * <i> )) by COMPLEX1:29
.= (p * (Re z)) + ((p * (Im z)) * <i> ) ;
hence ( Re ((p * <i> ) * z) = - (p * (Im z)) & Im ((p * <i> ) * z) = p * (Re z) & Re (p * z) = p * (Re z) & Im (p * z) = p * (Im z) ) by A1, COMPLEX1:28; :: thesis: verum