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: len (doms p) = len p by TREES_3:38;
now :: thesis: for x being object st x in dom (doms p) holds
(doms p) . x is finite Tree
let x be object ; :: 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 Nat such that
A3: ( x = i + 1 & i < len p ) by A2, Lm1;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A4: p . x = t | <*i*> by A1, A3, TREES_4:def 4;
( n in dom (t | <*i*>) & <*i*> ^ n = <*i*> ) by FINSEQ_1:34, TREES_1:22;
then reconsider ii = <*i*> as Node of t by A1, A3, A4, TREES_4:11;
x in dom p by A3, Lm3;
then (doms p) . x = dom (t | ii) by A4, FUNCT_6:22;
hence (doms p) . x is finite Tree ; :: thesis: verum
end;
then reconsider dp = doms p as FinTree-yielding FinSequence by TREES_3:23;
A5: dom t = tree dp by A1, TREES_4:10;
A6: ex q being Element of dom t st
( q = n & succ (t,n) = t * (q succ) ) by Def6;
rng (n succ) c= dom t ;
then dom (succ (t,n)) = dom (n succ) by A6, RELAT_1:27;
then A7: len (succ (t,n)) = len (n succ) by FINSEQ_3:29;
then A8: len (succ (t,n)) = card (succ n) by Def5
.= len p by A2, A5, Th29 ;
A9: now :: thesis: for i being Nat st i < len p holds
(succ (t,n)) . (i + 1) = (roots p) . (i + 1)
let i be 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)
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
i + 1 in dom p by Lm3, A10;
then A11: ( {} in (dom t) | <*ii*> & ex T being DecoratedTree st
( T = p . (i + 1) & (roots p) . (i + 1) = T . {} ) ) by TREES_1:22, TREES_3:def 18;
p . (i + 1) = t | <*ii*> by A1, A10, TREES_4:def 4;
then A12: (roots p) . (i + 1) = t . (<*i*> ^ {}) by A11, TREES_1:22, TREES_2:def 10;
i + 1 in dom (succ (t,n)) by A8, A10, Lm3;
then (succ (t,n)) . (i + 1) = t . ((n succ) . (i + 1)) by A6, FUNCT_1:12
.= t . (n ^ <*i*>) by A7, A8, A10, Def5
.= t . <*i*> by FINSEQ_1:34 ;
hence (succ (t,n)) . (i + 1) = (roots p) . (i + 1) by A12, FINSEQ_1:34; :: thesis: verum
end;
dom (roots p) = dom p by TREES_3:def 18;
then len (roots p) = len p by FINSEQ_3:29;
hence succ (t,n) = roots p by A8, A9, Lm2; :: thesis: verum