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