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 by FINSEQ_1:def 4;
hence dom (T * (t succ )) = dom (t succ ) by RELAT_1:46; :: thesis: verum