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

let z be set ; :: thesis:
assume A2: z in Seg (card A) ; :: thesis:
then reconsider m = z as Element of NAT ;
m >= 1 by A2, FINSEQ_1:3;
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 13;
reconsider y = t | <*n*> as set ;
take y ; :: thesis:
take n ; :: thesis:
thus ( n + 1 = z & y = t | <*n*> ) by A3; :: thesis:

end;

consider p being Function such that
A4: dom p = Seg (card A) and
A5: for z being set 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;

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

end;

then reconsider p = p as DTree-yielding FinSequence by TREES_3:26;
take p ; :: thesis:
reconsider e = {} as Element of dom t by TREES_1:47;

A7: now

let n be Element of NAT ; :: thesis:
thus ( e ^ <*n*> = <*n*> & succ e = A ) by FINSEQ_1:47, TREES_2:15; :: thesis:
hence ( <*n*> in A iff n < card A ) by Th7; :: thesis:

end;

A8: len (doms p) = len p by TREES_3:40;

let x be set ; :: thesis:

hereby :: thesis:

assume A9: ( x in dom t & x <> {} ) ; :: thesis:
then reconsider r = x as Node of t ;
consider q being FinSequence of NAT , n being Nat such that
A10: r = <*n*> ^ q by A9, FINSEQ_2:150;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
reconsider q = q as FinSequence ;
take n = n; :: thesis:
take q = q; :: thesis:
A11: ( <*n*> in dom t & e ^ <*n*> = <*n*> & succ e = A ) by A7, A10, TREES_1:46;
then <*n*> in A ;
hence K: n < len (doms p) by A6, A7, A8; :: thesis:
then A12: ( n + 1 in dom (doms p) & n + 1 in dom p ) by A8, Lm3;
consider k being Element of NAT such that
A13: ( k + 1 = n + 1 & p . (n + 1) = t | <*k*> ) by A4, A5, A8, Lm3, K;
(doms p) . (n + 1) = dom (t | <*n*>) by A12, A13, FUNCT_6:31
.= (dom t) | <*n*> by TREES_2:def 11 ;
hence ( q in (doms p) . (n + 1) & x = <*n*> ^ q ) by A10, A11, TREES_1:def 9; :: thesis:

end;

assume A14: ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) ) ; :: thesis:
assume A15: not x in dom t ; :: thesis:
then consider n being Element of NAT , q being FinSequence such that
A16: ( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) by A14, TREES_1:47;
A17: n + 1 in dom p by A8, A16, Lm3;
consider k being Element of NAT such that
A18: ( k + 1 = n + 1 & p . (n + 1) = t | <*k*> ) by A4, A5, A8, A16, Lm3;
(doms p) . (n + 1) = dom (t | <*n*>) by A17, A18, FUNCT_6:31
.= (dom t) | <*n*> by TREES_2:def 11 ;
then reconsider q = q as Element of (dom t) | <*n*> by A16;
( <*n*> in A & e ^ <*n*> = <*n*> & succ e = A ) by A6, A7, A8, A16;
then <*n*> ^ q in dom t by TREES_1:def 9;
hence contradiction by A15, A16; :: thesis:

end;

then A19: dom t = tree (doms p) by TREES_3:def 15;

let n be Element of NAT ; :: thesis:
assume n < len p ; :: thesis:
then consider m being Element of NAT such that
A20: ( m + 1 = n + 1 & p . (n + 1) = t | <*m*> ) by A4, A5, Lm3;
thus t | <*n*> = p . (n + 1) by A20; :: thesis:

end;

hence t = x -tree p by A19, TREES_4:def 4; :: thesis: