let x be set ; :: thesis: for p being DTree-yielding FinSequence holds rng p c= Subtrees (x -tree p)
let p be DTree-yielding FinSequence; :: thesis: rng p c= Subtrees (x -tree p)
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in Subtrees (x -tree p) )
assume z in rng p ; :: thesis: 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; :: thesis: verum