defpred S1[ 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 S1[q,x]
proof
let q be
FinSequence of
NAT ;
( q in tree ((dom T),P,(dom T1)) implies ex x being set st S1[q,x] )
assume
q in tree (
(dom T),
P,
(dom T1))
;
ex x being set st S1[q,x]
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;
hence
ex
x being
set st
S1[
q,
x]
by A3, A4, XBOOLE_0:def 3;
verum
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
S1[p,T0 . p] ) )
from TREES_2:sch 6(A2); verum