consider T2 being DecoratedTree such that
A2: T2 = tree T,P,T1 ;
T2 is ParametrizedSubset of D

proof

thus rng T2 c= D :: according to TREES_2:def 9 :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng T2 or y in D )
assume y in rng T2 ; :: thesis: y in D
then consider x being set such that
A3: ( x in dom T2 & y = T2 . x ) by FUNCT_1:def 5;
x is Element of dom T2 by A3;
then reconsider q = x as FinSequence of NAT ;
dom T2 = tree (dom T),P,(dom T1) by A1, A2, Def2;
then A4: dom T2 = { 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, 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 A3, A4, XBOOLE_0:def 3;

suppose A5: 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

then A6: (tree T,P,T1) . q = T . q by A1, A2, A3, Th15;

now

consider t' being Element of dom T such that
A7: ( q = t' & ( for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t' ) ) by A5;
thus q in dom T by A7; :: thesis: verum

end;

then A8: y in rng T by A2, A3, A6, FUNCT_1:def 5;
rng T c= D by TREES_2:def 9;
hence y in D by A8; :: thesis: verum

end;

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

then consider p being Element of dom T, r being Element of dom T1 such that
A9: ( q = p ^ r & p in P & (tree T,P,T1) . q = T1 . r ) by A2, A3, Th17;
thus y in D by A2, A3, A9; :: thesis: verum

end;

end;

end;

end;

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