set T = d -tree p;
rng (d -tree p) c= D
proof
let x be
object ;
TARSKI:def 3 ( not x in rng (d -tree p) or x in D )
assume
x in rng (d -tree p)
;
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 ( y <> {} implies x in D )assume
y <> {}
;
x in Dthen 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;
verum end;
hence
x in D
by A2, A4;
verum
end;
hence
d -tree p is D -valued
by RELAT_1:def 19; verum