dom (Re c) = dom c by Def1a
.= NAT by FUNCT_2:def 1 ;
then Re c is total by PARTFUN1:def 4;
hence Re c is Real_Sequence ; :: thesis: verum