reconsider e = {} as Element of dom T by TREES_1:22;
consider x being object such that
A1: x in succ e by XBOOLE_0:def 1;
reconsider x = x as Element of dom T by A1;
ex n being Nat st
( x = e ^ <*n*> & e ^ <*n*> in dom T ) by A1;
then T . x in rngr T ;
hence not rngr T is empty ; :: thesis: verum