dom (cosec f) = dom f by Def4;
hence len (cosec f) = len f by FINSEQ_3:29; :: according to CARD_1:def 7 :: thesis: verum