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