defpred S₁[ object , object ] means ex d being DecoratedTree ex p being FinSequence of Subtrees t st
( p = $2 & d = $1 & d = (d . {}) -tree p );
A1: for x being object st x in C -Subtrees t holds
ex y being object st
( y in (Subtrees t) * & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in C -Subtrees t implies ex y being object st
( y in (Subtrees t) * & S₁[x,y] ) )
assume x in C -Subtrees t ; :: thesis: ex y being object st
( y in (Subtrees t) * & S₁[x,y] )
then reconsider s = x as Element of Subtrees t ;
reconsider d = s as DecoratedTree ;
consider sp being Node of t such that
A2: s = t | sp by Th10;
consider z being set , p being DTree-yielding FinSequence such that
A3: s = z -tree p by Th8;
rng p c= Subtrees t

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in Subtrees t )
A4: dom (t | sp) = (dom t) | sp by TREES_2:def 10;
assume x in rng p ; :: thesis: x in Subtrees t
then consider k being Nat such that
A5: ( k < len p & x = p . (k + 1) ) by Lm4;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
reconsider e = {} as Node of (s | <*k*>) by TREES_1:22;
A6: x = s | <*k*> by A3, A5, TREES_4:def 4;
<*k*> ^ e = <*k*> by FINSEQ_1:34;
then <*k*> in dom s by A3, A5, A6, TREES_4:11;
then reconsider q = sp ^ <*k*> as Node of t by A2, A4, TREES_1:def 6;
x = t | q by A2, A6, Th3;
hence x in Subtrees t ; :: thesis: verum

end;

then reconsider p = p as FinSequence of Subtrees t by FINSEQ_1:def 4;
reconsider y = p as set ;
take y ; :: thesis: ( y in (Subtrees t) * & S₁[x,y] )
thus y in (Subtrees t) * by FINSEQ_1:def 11; :: thesis: S₁[x,y]
take d ; :: thesis: ex p being FinSequence of Subtrees t st
( p = y & d = x & d = (d . {}) -tree p )
take p ; :: thesis: ( p = y & d = x & d = (d . {}) -tree p )
thus ( p = y & d = x & d = (d . {}) -tree p ) by A3, TREES_4:def 4; :: thesis: verum

end;

consider f being Function such that
A7: ( dom f = C -Subtrees t & rng f c= (Subtrees t) * & ( for x being object st x in C -Subtrees t holds
S₁[x,f . x] ) ) from FUNCT_1:sch 6(A1);
reconsider f = f as Function of (C -Subtrees t),((Subtrees t) *) by A7, FUNCT_2:def 1, RELSET_1:4;
take f ; :: thesis: for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = f . d holds
d = (d . {}) -tree p
let d be DecoratedTree; :: thesis: ( d in C -Subtrees t implies for p being FinSequence of Subtrees t st p = f . d holds
d = (d . {}) -tree p )
assume d in C -Subtrees t ; :: thesis: for p being FinSequence of Subtrees t st p = f . d holds
d = (d . {}) -tree p
then ex d9 being DecoratedTree ex p being FinSequence of Subtrees t st
( p = f . d & d9 = d & d9 = (d9 . {}) -tree p ) by A7;
hence for p being FinSequence of Subtrees t st p = f . d holds
d = (d . {}) -tree p ; :: thesis: verum