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

end;

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