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