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

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