set T = d -flat_tree p;

rng (d -flat_tree p) c= D

rng (d -flat_tree p) c= D

proof

hence
d -flat_tree p is D -valued
by RELAT_1:def 19; :: thesis: verum
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;

end;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 )

hence
x in D
by A2, A4; :: thesis: verumassume
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;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