reconsider L = {} as T-Sequence ;
take L ; :: thesis: rng L c= Z
rng {} = {} ;
hence rng L c= Z by XBOOLE_1:2; :: thesis: verum