let q be DTree-yielding FinSequence; :: thesis: for k being Element of NAT st k + 1 in dom q holds
<*k*> in tree (doms q)
let k be Element of NAT ; :: thesis: ( k + 1 in dom q implies <*k*> in tree (doms q) )
assume A1: k + 1 in dom q ; :: thesis: <*k*> in tree (doms q)
then A2: k + 1 <= len q by FINSEQ_3:27;
k < k + 1 by XREAL_1:31;
then A3: k < len q by A2, XXREAL_0:2;
( dom (doms q) = dom q & doms q is Tree-yielding ) by TREES_3:39;
then (doms q) . (k + 1) is Tree by A1, TREES_3:24;
then A5: {} in (doms q) . (k + 1) by TREES_1:47;
( dom q = Seg (len q) & Seg (len (doms q)) = dom (doms q) ) by FINSEQ_1:def 3;
then A6: k < len (doms q) by A3, FINSEQ_1:8, TREES_3:39;
<*k*> = <*k*> ^ {} by FINSEQ_1:47;
hence <*k*> in tree (doms q) by A5, A6, TREES_3:def 15; :: thesis: verum