let x be FinSequence of COMPLEX ; :: thesis: for a being Complex holds dom (a * x) = dom x
let a be Complex; :: 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:27
.= dom (a * x) by SEQ_4:def 9 ;
:: thesis: verum