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