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