let z be complex number ; :: thesis: for r being Real holds cpx2euc (r * z) = r * (cpx2euc z)
let r be Real; :: thesis: cpx2euc (r * z) = r * (cpx2euc z)
r = r + (0 * <i> ) ;
then A1: ( Re r = r & Im r = 0 ) by COMPLEX1:28;
then A2: Re (r * z) = (r * (Re z)) - (0 * (Im z)) by COMPLEX1:24
.= r * (Re z) ;
A3: Im (r * z) = (r * (Im z)) + (0 * (Re z)) by A1, COMPLEX1:24
.= r * (Im z) ;
( (cpx2euc z) `1 = Re z & (cpx2euc z) `2 = Im z ) by EUCLID:56;
hence cpx2euc (r * z) = r * (cpx2euc z) by A2, A3, EUCLID:61; :: thesis: verum