let t be finite-branching DecoratedTree; :: thesis: ex x being set ex p being DTree-yielding FinSequence st t = x -tree p
take t . {} ; :: thesis: ex p being DTree-yielding FinSequence st t = (t . {}) -tree p
reconsider e = {} as Node of t by TREES_1:22;
defpred S₁[ object , object ] means ex n being Element of NAT st
( n + 1 = $1 & $2 = t | <*n*> );
(dom t) -level 1 = succ e by TREES_2:13;
then reconsider A = (dom t) -level 1 as finite set ;
reconsider e = {} as Element of dom t by TREES_1:22;
A1: for z being object st z in Seg (card A) holds
ex u being object st S₁[z,u]

proof

let z be object ; :: thesis: ( z in Seg (card A) implies ex u being object st S₁[z,u] )
assume A2: z in Seg (card A) ; :: thesis: ex u being object st S₁[z,u]
then reconsider m = z as Nat ;
m >= 1 by A2, FINSEQ_1:1;
then consider n being Nat such that
A3: m = 1 + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider y = t | <*n*> as set ;
take y ; :: thesis: S₁[z,y]
take n ; :: thesis: ( n + 1 = z & y = t | <*n*> )
thus ( n + 1 = z & y = t | <*n*> ) by A3; :: thesis: verum

end;

consider p being Function such that
A4: dom p = Seg (card A) and
A5: for z being object st z in Seg (card A) holds
S₁[z,p . z] from CLASSES1:sch 1(A1);
reconsider p = p as FinSequence by A4, FINSEQ_1:def 2;
A6: len p = card A by A4, FINSEQ_1:def 3;

A7: now :: thesis: for x being object st x in dom p holds
p . x is DecoratedTree

let x be object ; :: thesis: ( x in dom p implies p . x is DecoratedTree )
assume x in dom p ; :: thesis: p . x is DecoratedTree
then ex n being Element of NAT st
( n + 1 = x & p . x = t | <*n*> ) by A4, A5;
hence p . x is DecoratedTree ; :: thesis: verum

end;

A8: now :: thesis: for n being Nat holds
( e ^ <*n*> = <*n*> & succ e = A & ( <*n*> in A implies n < card A ) & ( n < card A implies <*n*> in A ) )

let n be Nat; :: thesis: ( e ^ <*n*> = <*n*> & succ e = A & ( <*n*> in A implies n < card A ) & ( n < card A implies <*n*> in A ) )
thus ( e ^ <*n*> = <*n*> & succ e = A ) by FINSEQ_1:34, TREES_2:13; :: thesis: ( <*n*> in A iff n < card A )
hence ( <*n*> in A iff n < card A ) by Th7; :: thesis: verum

end;

reconsider p = p as DTree-yielding FinSequence by A7, TREES_3:24;
A9: len (doms p) = len p by TREES_3:38;

now :: thesis: for x being object holds
( ( x in dom t & x <> {} implies ex nn being Nat ex q being FinSequence st
( nn < len (doms p) & q in (doms p) . (nn + 1) & x = <*nn*> ^ q ) ) & ( ( x = {} or ex n being Nat ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) ) implies x in dom t ) )

let x be object ; :: thesis: ( ( x in dom t & x <> {} implies ex nn being Nat ex q being FinSequence st
( nn < len (doms p) & q in (doms p) . (nn + 1) & x = <*nn*> ^ q ) ) & ( ( x = {} or ex n being Nat ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) ) implies x in dom t ) )

hereby :: thesis: ( ( x = {} or ex n being Nat ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) ) implies x in dom t )

assume that
A10: x in dom t and
A11: x <> {} ; :: thesis: ex nn being Nat ex q being FinSequence st
( nn < len (doms p) & q in (doms p) . (nn + 1) & x = <*nn*> ^ q )
reconsider r = x as Node of t by A10;
consider q being FinSequence of NAT , n being Element of NAT such that
A12: r = <*n*> ^ q by A11, FINSEQ_2:130;
A13: <*n*> in dom t by A12, TREES_1:21;
reconsider q = q as FinSequence ;
reconsider nn = n as Nat ;
take nn = nn; :: thesis: ex q being FinSequence st
( nn < len (doms p) & q in (doms p) . (nn + 1) & x = <*nn*> ^ q )
take q = q; :: thesis: ( nn < len (doms p) & q in (doms p) . (nn + 1) & x = <*nn*> ^ q )
e ^ <*n*> = <*n*> by A8;
then <*n*> in A by A8, A13;
hence nn < len (doms p) by A6, A8, A9; :: thesis: ( q in (doms p) . (nn + 1) & x = <*nn*> ^ q )
then ( n + 1 in dom p & ex k being Element of NAT st
( k + 1 = n + 1 & p . (n + 1) = t | <*k*> ) ) by A4, A5, A9, Lm3;
then (doms p) . (n + 1) = dom (t | <*n*>) by FUNCT_6:22
.= (dom t) | <*n*> by TREES_2:def 10 ;
hence ( q in (doms p) . (nn + 1) & x = <*nn*> ^ q ) by A12, A13, TREES_1:def 6; :: thesis: verum

end;

assume A14: ( x = {} or ex n being Nat ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) ) ; :: thesis: x in dom t
assume A15: not x in dom t ; :: thesis: contradiction
then consider n being Nat, q being FinSequence such that
A16: n < len (doms p) and
A17: q in (doms p) . (n + 1) and
A18: x = <*n*> ^ q by A14, TREES_1:22;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
( n + 1 in dom p & ex k being Element of NAT st
( k + 1 = n + 1 & p . (n + 1) = t | <*k*> ) ) by A4, A5, A9, A16, Lm3;
then (doms p) . (n + 1) = dom (t | <*n*>) by FUNCT_6:22
.= (dom t) | <*n*> by TREES_2:def 10 ;
then reconsider q = q as Element of (dom t) | <*n*> by A17;
<*n*> in A by A6, A8, A9, A16;
then <*n*> ^ q in dom t by TREES_1:def 6;
hence contradiction by A15, A18; :: thesis: verum

end;

then A19: dom t = tree (doms p) by TREES_3:def 15;
take p ; :: thesis: t = (t . {}) -tree p

now :: thesis: for n being Nat st n < len p holds
t | <*n*> = p . (n + 1)

let n be Nat; :: thesis: ( n < len p implies t | <*n*> = p . (n + 1) )
assume n < len p ; :: thesis: t | <*n*> = p . (n + 1)
then ex m being Element of NAT st
( m + 1 = n + 1 & p . (n + 1) = t | <*m*> ) by A4, A5, Lm3;
hence t | <*n*> = p . (n + 1) ; :: thesis: verum

end;

hence t = (t . {}) -tree p by A19, TREES_4:def 4; :: thesis: verum