reconsider w = T . t as Element of rng T by FUNCT_1:def 3;
reconsider w = w as consistent PNPair ;
succ (T,t) = the Enumeration of compn w by Def11;
then rng (succ (T,t)) = compn w by RLAFFIN3:def 1;
then consider y being object such that
A1: y in rng (succ (T,t)) by XBOOLE_0:def 1;
ex x being Element of dom T st
( y = T . x & x in succ t ) by TREES_9:42, A1;
hence not succ t is empty ; :: thesis: verum