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