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