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