let r be Real; :: thesis: for z being Element of COMPLEX holds
( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) )
let z be Element of 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:28;
r * z = (((Re r9) * (Re z)) - ((Im r9) * (Im z))) + ((((Re r9) * (Im z)) + ((Re z) * (Im r9))) * <i> ) by COMPLEX1:def 10
.= (r * (Re z)) + ((r * (Im z)) * <i> ) by A1 ;
hence ( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) ) by COMPLEX1:28; :: thesis: verum