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