let z be complex number ; :: thesis: for r being real number holds
( Re (r * z) = r * (Re z) & Im (r * z) = r * (Im z) )
let r be real number ; :: thesis: ( Re (r * z) = r * (Re z) & Im (r * z) = r * (Im z) )
A1: r in REAL by XREAL_0:def 1;
then 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 A1, 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 A1, COMPLEX1:def 2
.= r * (Im z) ; :: thesis: verum