let f be real-valued FinSequence; :: thesis: len (cot f) = len f
dom (cot f) = dom f by Def3;
hence len (cot f) = len f by FINSEQ_3:29; :: thesis: verum