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 )
consider q being Element of dom T such that
A1: ( q = t & succ T,t = T * (q succ ) ) by TREES_9:def 6;
thus succ T,t = T * (t succ ) by A1; :: thesis: verum