let T be finite-branching DecoratedTree; :: thesis: for t being Element of dom T holds succ T,t = T * (t succ )
let t be Element of dom T; :: thesis: succ T,t = T * (t succ )
ex q being Element of dom T st
( q = t & succ T,t = T * (q succ ) ) by Def6;
hence succ T,t = T * (t succ ) ; :: thesis: verum