set X = T with-replacement (p,T1);
rng (T with-replacement (p,T1)) c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (T with-replacement (p,T1)) or x in D )
assume x in rng (T with-replacement (p,T1)) ; :: thesis: x in D
then consider z being object such that
A2: z in dom (T with-replacement (p,T1)) and
A3: x = (T with-replacement (p,T1)) . z by FUNCT_1:def 3;
reconsider z = z as FinSequence of NAT by A2, TREES_1:19;
A4: dom (T with-replacement (p,T1)) = (dom T) with-replacement (p,(dom T1)) by A1, TREES_2:def 11;

now :: thesis: x in D

per cases ( ( not p is_a_prefix_of z & (T with-replacement (p,T1)) . z = T . z ) or ex s being FinSequence of NAT st
( s in dom T1 & z = p ^ s & (T with-replacement (p,T1)) . z = T1 . s ) ) by A1, A2, A4, TREES_2:def 11;

suppose A5: ( not p is_a_prefix_of z & (T with-replacement (p,T1)) . z = T . z ) ; :: thesis: x in D

then for s being FinSequence of NAT holds
( not s in dom T1 or not z = p ^ s ) by TREES_1:1;
then reconsider z = z as Element of dom T by A1, A2, A4, TREES_1:def 9;
T . z is Element of D ;
hence x in D by A3, A5; :: thesis: verum

end;

suppose ex s being FinSequence of NAT st
( s in dom T1 & z = p ^ s & (T with-replacement (p,T1)) . z = T1 . s ) ; :: thesis: x in D

then consider s being FinSequence of NAT such that
A6: s in dom T1 and
z = p ^ s and
A7: (T with-replacement (p,T1)) . z = T1 . s ;
reconsider s = s as Element of dom T1 by A6;
T1 . s is Element of D ;
hence x in D by A3, A7; :: thesis: verum

end;

end;

end;

hence x in D ; :: thesis: verum

end;

hence T with-replacement (p,T1) is DecoratedTree of D by RELAT_1:def 19; :: thesis: verum