let T be finite-branching DecoratedTree; :: thesis: for t being Element of dom T holds dom (succ T,t) = dom (t succ )
let t be Element of dom T; :: thesis: dom (succ T,t) = dom (t succ )
thus dom (succ T,t) = dom (T * (t succ )) by Th9
.= dom (t succ ) by Th10 ; :: thesis: verum