let D be set ; :: thesis: {} is XFinSequence of
rng {} c= D by XBOOLE_1:2;
hence {} is XFinSequence of by RELAT_1:def 19; :: thesis: verum