dom f = dom (r |^ f) by Def4;
then len f = len (r |^ f) by FINSEQ_3:29;
hence r |^ f is len f -element by CARD_1:def 7; :: thesis: verum