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