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

( 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