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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (d -flat_tree p) or x in D )
assume x in rng (d -flat_tree p) ; :: thesis: x in D
then consider y being object such that
A1: y in dom (d -flat_tree p) and
A2: x = (d -flat_tree p) . y by FUNCT_1:def 3;
reconsider y = y as Node of (d -flat_tree p) by A1;
A3: dom (d -flat_tree p) = elementary_tree (len p) by Def3;
A4: (d -flat_tree p) . {} = d by Def3;

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

assume y <> {} ; :: thesis: x in D
then consider n being Nat such that
A5: ( n < len p & y = <*n*> ) by A3, TREES_1:30;
A6: ( (d -flat_tree p) . y = p . (n + 1) & p . (n + 1) in rng p ) by A5, Def3, Lm2;
rng p c= D by FINSEQ_1:def 4;
hence x in D by A2, A6; :: thesis: verum

end;

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

end;

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