let f be complex-valued FinSequence; :: thesis: len (f ") = len f
dom (f ") = dom f by VALUED_1:def 7;
hence len (f ") = len f by FINSEQ_3:29; :: thesis: verum