let r be Real; :: thesis: for p being Point of (TOP-REAL 2) holds euc2cpx (r * p) = r * (euc2cpx p)
let p be Point of (TOP-REAL 2); :: thesis: euc2cpx (r * p) = r * (euc2cpx p)
r * p = |[(r * (p `1 )),(r * (p `2 ))]| by EUCLID:61;
then ( (r * p) `1 = r * (p `1 ) & (r * p) `2 = r * (p `2 ) ) by EUCLID:56;
then euc2cpx (r * p) = (r + (0 * <i> )) * ((p `1 ) + ((p `2 ) * <i> )) ;
hence euc2cpx (r * p) = r * (euc2cpx p) ; :: thesis: verum