set T = d -tree p;

rng (d -tree p) c= D

rng (d -tree p) c= D

proof

hence
d -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 -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;

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

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

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;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 ) by FINSEQ_1:40;

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