let a be real number ; :: thesis: for z being complex number holds Re (a * z) = a * (Re z)
let z be complex number ; :: thesis: Re (a * z) = a * (Re z)
A1: a in REAL by XREAL_0:def 1;
Re (a * z) = ((Re a) * (Re z)) - ((Im a) * (Im z)) by COMPLEX1:24
.= ((Re a) * (Re z)) - (0 * (Im z)) by A1, COMPLEX1:def 3
.= a * (Re z) by A1, COMPLEX1:def 2 ;
hence Re (a * z) = a * (Re z) ; :: thesis: verum