let r be Real; :: thesis: for z being Complex holds
( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) )
let z be Complex; :: thesis: ( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) )
reconsider r9 = r as Element of COMPLEX by XCMPLX_0:def 2;
r = r + (0 * <i>) ;
then A1: ( Re r = r & Im r = 0 ) by COMPLEX1:12;
r * z = (((Re r9) * (Re z)) - ((Im r9) * (Im z))) + ((((Re r9) * (Im z)) + ((Re z) * (Im r9))) * <i>) by COMPLEX1:82
.= (r * (Re z)) + ((r * (Im z)) * <i>) by A1 ;
hence ( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) ) by COMPLEX1:12; :: thesis: verum