let t be finite DecoratedTree; :: thesis: for x being set
for p being DTree-yielding FinSequence st t = x -tree p holds
for n being empty Element of dom t holds succ t,n = roots p
let x be set ; :: thesis: for p being DTree-yielding FinSequence st t = x -tree p holds
for n being empty Element of dom t holds succ t,n = roots p
let p be DTree-yielding FinSequence; :: thesis: ( t = x -tree p implies for n being empty Element of dom t holds succ t,n = roots p )
assume A1: t = x -tree p ; :: thesis: for n being empty Element of dom t holds succ t,n = roots p
let n be empty Element of dom t; :: thesis: succ t,n = roots p
A2: ex q being Element of dom t st
( q = n & succ t,n = t * (q succ ) ) by Def6;
dom (roots p) = dom p by TREES_3:def 18;
then A3: len (roots p) = len p by FINSEQ_3:31;
A4: len (doms p) = len p by TREES_3:40;

now

let x be set ; :: thesis: ( x in dom (doms p) implies (doms p) . x is finite Tree )
assume x in dom (doms p) ; :: thesis: (doms p) . x is finite Tree
then consider i being Element of NAT such that
A5: ( x = i + 1 & i < len p ) by A4, Lm1;
A6: ( p . x = t | <*i*> & n in dom (t | <*i*>) & <*i*> ^ n = <*i*> ) by A1, A5, FINSEQ_1:47, TREES_1:47, TREES_4:def 4;
then reconsider ii = <*i*> as Node of t by A1, A5, TREES_4:11;
x in dom p by A5, Lm3;
then (doms p) . x = dom (t | ii) by A6, FUNCT_6:31;
hence (doms p) . x is finite Tree ; :: thesis: verum

end;

then reconsider dp = doms p as FinTree-yielding FinSequence by TREES_3:25;
A7: dom t = tree dp by A1, TREES_4:10;
rng (n succ ) c= dom t ;
then dom (succ t,n) = dom (n succ ) by A2, RELAT_1:46;
then A8: len (succ t,n) = len (n succ ) by FINSEQ_3:31;
then A9: len (succ t,n) = card (succ n) by Def5
.= len p by A4, A7, Th30 ;

now

let i be Element of NAT ; :: thesis: ( i < len p implies (succ t,n) . (i + 1) = (roots p) . (i + 1) )
assume A10: i < len p ; :: thesis: (succ t,n) . (i + 1) = (roots p) . (i + 1)
then A11: ( p . (i + 1) = t | <*i*> & {} in (dom t) | <*i*> ) by A1, TREES_1:47, TREES_4:def 4;
i + 1 in dom (succ t,n) by A9, A10, Lm3;
then A12: (succ t,n) . (i + 1) = t . ((n succ ) . (i + 1)) by A2, FUNCT_1:22
.= t . (n ^ <*i*>) by A8, A9, A10, Def5
.= t . <*i*> by FINSEQ_1:47 ;
i + 1 in dom p by A10, Lm3;
then ex T being DecoratedTree st
( T = p . (i + 1) & (roots p) . (i + 1) = T . {} ) by TREES_3:def 18;
then (roots p) . (i + 1) = t . (<*i*> ^ {} ) by A11, TREES_1:47, TREES_2:def 11;
hence (succ t,n) . (i + 1) = (roots p) . (i + 1) by A12, FINSEQ_1:47; :: thesis: verum

end;

hence succ t,n = roots p by A3, A9, Lm2; :: thesis: verum