let x be FinSequence of COMPLEX ; :: thesis: dom x = dom (- x)
dom compcomplex = COMPLEX by FUNCT_2:def 1;
then rng x c= dom compcomplex by FINSEQ_1:def 4;
hence dom x = dom (compcomplex * x) by RELAT_1:46
.= dom (- x) by COMPLSP1:def 9 ;
:: thesis: verum