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 ) )
A1: ex q being Element of dom t st
( q = p & succ t,p = t * (q succ ) ) by Def6;
rng (p succ ) c= dom t ;
then dom (succ t,p) = dom (p succ ) by A1, RELAT_1:46;
hence ( len (succ t,p) = len (p succ ) & dom (succ t,p) = dom (p succ ) ) by FINSEQ_3:31; :: thesis: verum