let q be DTree-yielding FinSequence; for k being Nat st k + 1 in dom q holds
<*k*> in tree (doms q)
let k be Nat; ( 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
; <*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; verum