let T be finite-branching DecoratedTree; :: thesis: for t being Element of dom T holds dom (T * (t succ)) = dom (t succ)
let t be Element of dom T; :: thesis: dom (T * (t succ)) = dom (t succ)
rng (t succ) c= dom T ;
hence dom (T * (t succ)) = dom (t succ) by RELAT_1:27; :: thesis: verum