set T = d -tree p;
rng (d -tree p) c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (d -tree p) or x in D )
assume x in rng (d -tree p) ; :: thesis: x in D
then consider y being object such that
A1: y in dom (d -tree p) and
A2: x = (d -tree p) . y by FUNCT_1:def 3;
reconsider y = y as Node of (d -tree p) by A1;
A3: (tree (doms p)) -level 1 = { <*n*> where n is Nat : n < len (doms p) } by TREES_3:49;
A4: (d -tree p) . {} = d by Def4;
A5: ( tree (doms p) = dom (d -tree p) & len (doms p) = len p ) by Th10, TREES_3:38;

now :: thesis: ( y <> {} implies x in D )

assume y <> {} ; :: thesis: x in D
then consider q being FinSequence of NAT , n being Element of NAT such that
A6: y = <*n*> ^ q by FINSEQ_2:130;
A7: <*n*> in dom (d -tree p) by A6, TREES_1:21;
A8: len <*n*> = 1 by FINSEQ_1:40;
A9: q in (dom (d -tree p)) | <*n*> by A6, A7, TREES_1:def 6;
A10: <*n*> in (dom (d -tree p)) -level 1 by A7, A8;
A11: dom ((d -tree p) | <*n*>) = (dom (d -tree p)) | <*n*> by TREES_2:def 10;
consider i being Nat such that
A12: ( <*n*> = <*i*> & i < len p ) by A3, A5, A10;
A13: ( <*n*> . 1 = n & <*i*> . 1 = i ) ;
then A14: (d -tree p) | <*n*> = p . (n + 1) by A12, Def4;
A15: p . (n + 1) in rng p by A12, A13, Lm2;
rng p c= F by FINSEQ_1:def 4;
then reconsider t = p . (n + 1) as Element of F by A15;
A16: t . q = x by A2, A6, A9, A14, TREES_2:def 10;
A17: t . q in rng t by A9, A11, A14, FUNCT_1:def 3;
rng t c= D by RELAT_1:def 19;
hence x in D by A16, A17; :: thesis: verum

end;

hence x in D by A2, A4; :: thesis: verum

end;

hence d -tree p is D -valued by RELAT_1:def 19; :: thesis: verum