dom (Im c) = dom c by Def4
.= NAT by FUNCT_2:def 1 ;
then Im c is total by PARTFUN1:def 2;
hence Im c is Real_Sequence ; :: thesis: verum