let x be FinSequence of COMPLEX ; :: thesis: len (- x) = len x
dom (- x) = dom x by Th4;
then Seg (len (- x)) = dom x by FINSEQ_1:def 3;
hence len (- x) = len x by FINSEQ_1:def 3; :: thesis: verum