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