let D, D9 be non empty set ; :: thesis:
assume that
A1: for x being set st x in D9 holds
x is DecoratedTree of D and
A2: D9 is c=-linear ; :: thesis:
for x being set st x in D9 holds
x is DecoratedTree by A1;
then reconsider T = union D9 as DecoratedTree by A2, Th35;
rng T c= D

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng T ; :: thesis:
then consider y being object such that
A3: ( y in dom T & x = T . y ) by FUNCT_1:def 3;
[y,x] in T by A3, FUNCT_1:1;
then consider X being set such that
A4: [y,x] in X and
A5: X in D9 by TARSKI:def 4;
reconsider X = X as DecoratedTree of D by A1, A5;
( y in dom X & x = X . y ) by A4, FUNCT_1:1;
then A6: x in rng X by FUNCT_1:def 3;
thus x in D by A6; :: thesis:

end;