dom (Re f) = dom f by COMSEQ_3:def 3;
hence ( Re f is real-valued & Re f is finite & Re f is Sequence-like ) by AFINSQ_1:5; :: thesis: verum