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

dom (- x) = dom x by VALUED_1:8;

hence len (- x) = len x by FINSEQ_3:29; :: thesis: verum