let z be Complex; :: thesis: for r being Real holds cpx2euc (r * z) = r * (cpx2euc z)
let r be Real; :: thesis: cpx2euc (r * z) = r * (cpx2euc z)
A1: ( (cpx2euc z) `1 = Re z & (cpx2euc z) `2 = Im z ) by EUCLID:52;
r = r + (0 * <i>) ;
then A2: ( Re r = r & Im r = 0 ) by COMPLEX1:12;
then A3: Im (r * z) = (r * (Im z)) + (0 * (Re z)) by COMPLEX1:9
.= r * (Im z) ;
Re (r * z) = (r * (Re z)) - (0 * (Im z)) by A2, COMPLEX1:9
.= r * (Re z) ;
hence cpx2euc (r * z) = r * (cpx2euc z) by A3, A1, EUCLID:57; :: thesis: verum