dom (Sum f) = dom f by Def8;
then len (Sum f) = len f by FINSEQ_3:29;
hence Sum f is len f -element by CARD_1:def 7; :: thesis: verum