let f be complex-valued FinSequence; :: thesis: len (- f) = len f
Seg (len (- f)) = dom (- f) by FINSEQ_1:def 3
.= dom f by VALUED_1:def 5
.= Seg (len f) by FINSEQ_1:def 3 ;
hence len (- f) = len f by FINSEQ_1:6; :: thesis: verum