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

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