set T = d -tree p;
A1:
rng (d -tree p) c= D
proof
let x be
set ;
TARSKI:def 3 ( not x in rng (d -tree p) or x in D )
assume A2:
x in rng (d -tree p)
;
x in D
consider y being
set such that A3:
y in dom (d -tree p)
and A4:
x = (d -tree p) . y
by A2, FUNCT_1:def 5;
reconsider y =
y as
Node of
(d -tree p) by A3;
A5:
(tree (doms p)) -level 1
= { <*n*> where n is Element of NAT : n < len (doms p) }
by TREES_3:52;
A6:
(d -tree p) . {} = d
by Def4;
A7:
(
tree (doms p) = dom (d -tree p) &
len (doms p) = len p )
by Th10, TREES_3:40;
A8:
now assume A9:
y <> {}
;
x in Dconsider q being
FinSequence of
NAT ,
n being
Nat such that A10:
y = <*n*> ^ q
by A9, FINSEQ_2:150;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
A11:
<*n*> in dom (d -tree p)
by A10, TREES_1:46;
A12:
len <*n*> = 1
by FINSEQ_1:57;
A13:
q in (dom (d -tree p)) | <*n*>
by A10, A11, TREES_1:def 9;
A14:
<*n*> in (dom (d -tree p)) -level 1
by A11, A12;
A15:
dom ((d -tree p) | <*n*>) = (dom (d -tree p)) | <*n*>
by TREES_2:def 11;
consider i being
Element of
NAT such that A16:
(
<*n*> = <*i*> &
i < len p )
by A5, A7, A14;
A17:
(
<*n*> . 1
= n &
<*i*> . 1
= i )
by FINSEQ_1:57;
A18:
(d -tree p) | <*n*> = p . (n + 1)
by A16, A17, Def4;
A19:
p . (n + 1) in rng p
by A16, A17, Lm2;
A20:
rng p c= F
by FINSEQ_1:def 4;
reconsider t =
p . (n + 1) as
Element of
F by A19, A20;
A21:
t . q = x
by A4, A10, A13, A18, TREES_2:def 11;
A22:
t . q in rng t
by A13, A15, A18, FUNCT_1:def 5;
A23:
rng t c= D
by RELAT_1:def 19;
thus
x in D
by A21, A22, A23;
verum end;
thus
x in D
by A4, A6, A8;
verum
end;
thus
d -tree p is DecoratedTree of D
by A1, RELAT_1:def 19; verum