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

proof

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

A7: now

assume A8: y <> {} ; :: thesis: x in D
consider n being Element of NAT such that
A9: ( n < len p & y = <*n*> ) by A5, A8, TREES_1:57;
A10: ( (d -flat_tree p) . y = p . (n + 1) & p . (n + 1) in rng p ) by A9, Def3, Lm2;
A11: rng p c= D by FINSEQ_1:def 4;
thus x in D by A4, A10, A11; :: thesis: verum

end;

thus x in D by A4, A6, A7; :: thesis: verum

end;

thus d -flat_tree p is DecoratedTree of D by A1, RELAT_1:def 19; :: thesis: verum