let p be Real; :: thesis: for z being Complex 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; :: 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:13
.= (- (p * (Im z))) + ((p * (Re z)) * <i>) ;
p * z = p * ((Re z) + ((Im z) * <i>)) by COMPLEX1:13
.= (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:12; :: thesis: verum