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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng T or x in D )
assume x in rng T ; :: thesis: x in D
then consider y being set such that
A3: ( y in dom T & x = T . y ) by FUNCT_1:def 5;
( [y,x] in T & T = T ) by A3, FUNCT_1:8;
then consider X being set such that
A4: ( [y,x] in X & X in D' ) by TARSKI:def 4;
reconsider X = X as DecoratedTree of D by A1, A4;
( y in dom X & x = X . y ) by A4, FUNCT_1:8;
then ( x in rng X & rng X c= D ) by Def9, FUNCT_1:def 5;
hence x in D ; :: thesis: verum

end;

hence union D' is DecoratedTree of D by Def9; :: thesis: verum