let t be finite DecoratedTree; :: thesis: for p being Element of dom t holds
( len (succ (t,p)) = len (p succ) & dom (succ (t,p)) = dom (p succ) )
let p be Element of dom t; :: thesis: ( len (succ (t,p)) = len (p succ) & dom (succ (t,p)) = dom (p succ) )
( ex q being Element of dom t st
( q = p & succ (t,p) = t * (q succ) ) & rng (p succ) c= dom t ) by Def6;
then dom (succ (t,p)) = dom (p succ) by RELAT_1:27;
hence ( len (succ (t,p)) = len (p succ) & dom (succ (t,p)) = dom (p succ) ) by FINSEQ_3:29; :: thesis: verum