let x be FinSequence of COMPLEX ; :: thesis: for a being complex number holds dom (a * x) = dom x
let a be complex number ; :: thesis: dom (a * x) = dom x
dom (a multcomplex ) = COMPLEX by FUNCT_2:def 1;
then rng x c= dom (a multcomplex ) by FINSEQ_1:def 4;
hence dom x = dom ((a multcomplex ) * x) by RELAT_1:46
.= dom (a * x) by SEQ_4:def 12 ;
:: thesis: verum