theorem :: RVSUM_4:36

for f being XFinSequence holds f is XFinSequence of (rng f) \/ {1} by RELAT_1:def 19, XBOOLE_1:7;