let D9, D 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
A3: for x being set st x in D9 holds
x is DecoratedTree by A1;
reconsider T = union D9 as DecoratedTree by A2, A3, Th37;
A4: 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 A5: x in rng T ; :: thesis: x in D
consider y being set such that
A6: ( y in dom T & x = T . y ) by A5, FUNCT_1:def 5;
A7: [y,x] in T by A6, FUNCT_1:8;
consider X being set such that
A8: [y,x] in X and
A9: X in D9 by A7, TARSKI:def 4;
reconsider X = X as DecoratedTree of D by A1, A9;
A10: ( y in dom X & x = X . y ) by A8, FUNCT_1:8;
A11: x in rng X by A10, FUNCT_1:def 5;
A12: rng X c= D by RELAT_1:def 19;
thus x in D by A11, A12; :: thesis: verum

end;

thus union D9 is DecoratedTree of D by A4, RELAT_1:def 19; :: thesis: verum