let x be set ; for p being DTree-yielding FinSequence holds rng p c= Subtrees (x -tree p)
let p be DTree-yielding FinSequence; rng p c= Subtrees (x -tree p)
let z be object ; TARSKI:def 3 ( not z in rng p or z in Subtrees (x -tree p) )
assume
z in rng p
; z in Subtrees (x -tree p)
then consider y being object such that
A1:
( y in dom p & z = p . y )
by FUNCT_1:def 3;
reconsider y = y as Nat by A1;
consider i being Nat such that
A2:
y = 1 + i
by A1, FINSEQ_3:25, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
y <= len p
by A1, FINSEQ_3:25;
then A3:
i < len p
by A2, NAT_1:13;
then A4:
z = (x -tree p) | <*i*>
by A1, A2, TREES_4:def 4;
then reconsider z = z as DecoratedTree ;
reconsider q = {} as Element of dom z by TREES_1:22;
( dom (x -tree p) = tree (doms p) & dom z = (doms p) . y & len (doms p) = len p )
by A1, FUNCT_6:22, TREES_4:10, TREES_3:38;
then
<*i*> ^ q in dom (x -tree p)
by A2, A3, TREES_3:def 15;
then
<*i*> in dom (x -tree p)
by FINSEQ_1:34;
hence
z in Subtrees (x -tree p)
by A4; verum