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