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