set T2 = tree T,P,T1;
A2: tree T,P,T1 is D -valued

proof

let y be set ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in proj2 (tree T,P,T1) or y in D )
assume A3: y in rng (tree T,P,T1) ; :: thesis: y in D
consider x being set such that
A4: x in dom (tree T,P,T1) and
A5: y = (tree T,P,T1) . x by A3, FUNCT_1:def 5;
A6: x is Element of dom (tree T,P,T1) by A4;
reconsider q = x as FinSequence of NAT by A6;
A7: dom (tree T,P,T1) = tree (dom T),P,(dom T1) by A1, Def2;
A8: dom (tree T,P,T1) = { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } \/ { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } by A1, A7, Th7;

per cases ( q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } or q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } ) by A4, A8, XBOOLE_0:def 3;

suppose A9: q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } ; :: thesis: y in D

A10: (tree T,P,T1) . q = T . q by A1, A4, A9, Th15;

A11: now

A12: ex t9 being Element of dom T st
( q = t9 & ( for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t9 ) ) by A9;
thus q in dom T by A12; :: thesis: verum

end;

A13: y in rng T by A5, A10, A11, FUNCT_1:def 5;
A14: rng T c= D by RELAT_1:def 19;
thus y in D by A13, A14; :: thesis: verum

end;

suppose A15: q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } ; :: thesis: y in D

A16: ex p being Element of dom T ex r being Element of dom T1 st
( q = p ^ r & p in P & (tree T,P,T1) . q = T1 . r ) by A4, A15, Th17;
thus y in D by A5, A16; :: thesis: verum

end;

end;

end;

thus tree T,P,T1 is DecoratedTree of D by A2; :: thesis: verum