let Z be set ; :: thesis: {} is T-Sequence of Z
reconsider F = {} as Function ;
reconsider L = F as T-Sequence ;
rng L = {} ;
then rng L c= Z by XBOOLE_1:2;
hence {} is T-Sequence of Z by Def8; :: thesis: verum