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