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 Th36
.= dom (t succ) by Th37 ; :: thesis: verum