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