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

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in Subtrees X )
A5: dom (t | sp) = (dom t) | sp by TREES_2:def 10;
assume x in rng p ; :: thesis: x in Subtrees X
then consider k being Nat such that
A6: ( 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;
A7: x = s | <*k*> by A4, A6, TREES_4:def 4;
<*k*> ^ e = <*k*> by FINSEQ_1:34;
then <*k*> in dom s by A4, A6, A7, TREES_4:11;
then reconsider q = sp ^ <*k*> as Node of t by A3, A5, TREES_1:def 6;
x = t | q by A3, A7, Th3;
hence x in Subtrees X ; :: thesis: verum

end;

then reconsider p = p as FinSequence of Subtrees X by FINSEQ_1:def 4;
reconsider y = p as set ;
take y ; :: thesis: ( y in (Subtrees X) * & S₁[x,y] )
thus y in (Subtrees X) * by FINSEQ_1:def 11; :: thesis: S₁[x,y]
take d ; :: thesis: ex p being FinSequence of Subtrees X 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 A4, TREES_4:def 4; :: thesis: verum

end;

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