defpred S₁[ FinSequence, set ] means ( for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of $1 & $2 = T . $1 ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & $1 = p ^ r & $2 = T1 . r ) );
A2: for q being FinSequence of NAT st q in tree ((dom T),P,(dom T1)) holds
ex x being set st S₁[q,x]

proof

let q be FinSequence of NAT ; :: thesis:
assume q in tree ((dom T),P,(dom T1)) ; :: thesis:
then A3: q in { t where t is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t } \/ { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } by A1, Th7;

A4: now :: thesis:

assume q in { t where t is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t } ; :: thesis:
then consider t being Element of dom T such that
A5: ( q = t & ( for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t ) ) ;
take x = T . t; :: thesis:
for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & x = T . q ) by A5;
hence ex x being set st S₁[q,x] ; :: thesis:

end;

now :: thesis:

assume q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } ; :: thesis:
then consider p being Element of dom T, s being Element of dom T1 such that
A6: ( q = p ^ s & p in P ) ;
take x = T1 . s; :: thesis:
( for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & x = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & x = T1 . r ) ) by A6;
hence ex x being set st S₁[q,x] ; :: thesis:

end;

hence ex x being set st S₁[q,x] by A3, A4, XBOOLE_0:def 3; :: thesis:

end;

thus ex T0 being DecoratedTree st
( dom T0 = tree ((dom T),P,(dom T1)) & ( for p being FinSequence of NAT st p in tree ((dom T),P,(dom T1)) holds
S₁[p,T0 . p] ) ) from TREES_2:sch 6(A2); :: thesis: