let x be complex-valued FinSequence; :: thesis: len (- x) = len x
dom (- x) = dom x by VALUED_1:8;
hence len (- x) = len x by FINSEQ_3:29; :: thesis: verum