let D, D9 be non empty set ; :: thesis: ( ( for x being set st x in D9 holds
x is DecoratedTree of D ) & D9 is c=-linear implies union D9 is DecoratedTree of D )
assume that
A1: for x being set st x in D9 holds
x is DecoratedTree of D and
A2: D9 is c=-linear ; :: thesis: union D9 is DecoratedTree of D
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

proof

let x be object ; :: 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 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: verum

end;

hence union D9 is DecoratedTree of D by RELAT_1:def 19; :: thesis: verum