let q be DTree-yielding FinSequence; :: thesis: for k being Nat st k + 1 in dom q holds

<*k*> in tree (doms q)

let k be Nat; :: thesis: ( k + 1 in dom q implies <*k*> in tree (doms q) )

A1: k < k + 1 by XREAL_1:29;

A2: ( dom q = Seg (len q) & Seg (len (doms q)) = dom (doms q) ) by FINSEQ_1:def 3;

assume A3: k + 1 in dom q ; :: thesis: <*k*> in tree (doms q)

then k + 1 <= len q by FINSEQ_3:25;

then k < len q by A1, XXREAL_0:2;

then A4: k < len (doms q) by A2, FINSEQ_1:6, TREES_3:37;

dom (doms q) = dom q by TREES_3:37;

then (doms q) . (k + 1) is Tree by A3, TREES_3:22;

then A5: {} in (doms q) . (k + 1) by TREES_1:22;

<*k*> = <*k*> ^ {} by FINSEQ_1:34;

hence <*k*> in tree (doms q) by A5, A4, TREES_3:def 15; :: thesis: verum

<*k*> in tree (doms q)

let k be Nat; :: thesis: ( k + 1 in dom q implies <*k*> in tree (doms q) )

A1: k < k + 1 by XREAL_1:29;

A2: ( dom q = Seg (len q) & Seg (len (doms q)) = dom (doms q) ) by FINSEQ_1:def 3;

assume A3: k + 1 in dom q ; :: thesis: <*k*> in tree (doms q)

then k + 1 <= len q by FINSEQ_3:25;

then k < len q by A1, XXREAL_0:2;

then A4: k < len (doms q) by A2, FINSEQ_1:6, TREES_3:37;

dom (doms q) = dom q by TREES_3:37;

then (doms q) . (k + 1) is Tree by A3, TREES_3:22;

then A5: {} in (doms q) . (k + 1) by TREES_1:22;

<*k*> = <*k*> ^ {} by FINSEQ_1:34;

hence <*k*> in tree (doms q) by A5, A4, TREES_3:def 15; :: thesis: verum