dom (Im f) = dom f by COMSEQ_3:def 4;
hence Im f is len f -element by CARD_1:def 7; :: thesis: verum