let a be Real; :: thesis: for z being Complex holds Im (a * z) = a * (Im z)
let z be Complex; :: thesis: Im (a * z) = a * (Im z)
Im (a * z) = ((Re a) * (Im z)) + ((Re z) * (Im a)) by COMPLEX1:9
.= ((Re a) * (Im z)) + ((Re z) * 0) by COMPLEX1:def 2
.= a * (Im z) by COMPLEX1:def 1 ;
hence Im (a * z) = a * (Im z) ; :: thesis: verum