set g = (NAT --> 0) +* (f | X);
A0: dom ((NAT --> 0) +* (f | X)) = (dom (NAT --> 0)) \/ (dom (f | X)) by FUNCT_4:def 1
.= NAT \/ (dom (f | X)) ;
dom f = NAT by FUNCT_2:def 1;
then dom (f | X) = X by RELAT_1:62;
then A1: dom ((NAT --> 0) +* (f | X)) = NAT by XBOOLE_1:12, A0;
rng ((NAT --> 0) +* (f | X)) c= REAL ;
hence (NAT --> 0) +* (f | X) is Real_Sequence by A1, FUNCT_2:2; :: thesis: verum