let D be non empty set ; :: thesis: ( ( for x being set st x in D holds
x is DecoratedTree ) & D is c=-linear implies union D is DecoratedTree )
assume that
A1: for x being set st x in D holds
x is DecoratedTree and
A2: D is c=-linear ; :: thesis: union D is DecoratedTree
for x being set st x in D holds
x is Function by A1;
then reconsider T = union D as Function by A2, Th36;
defpred S₁[ set , set ] means ex T1 being DecoratedTree st
( $1 = T1 & dom T1 = $2 );
A3: for x being set st x in D holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in D implies ex y being set st S₁[x,y] )
assume x in D ; :: thesis: ex y being set st S₁[x,y]
then reconsider T1 = x as DecoratedTree by A1;
dom T1 = dom T1 ;
hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

consider f being Function such that
A4: ( dom f = D & ( for x being set st x in D holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A3);
reconsider E = rng f as non empty set by A4, RELAT_1:42;

now

let x be set ; :: thesis: ( x in E implies x is Tree )
assume x in E ; :: thesis: x is Tree
then consider y being set such that
A5: ( y in dom f & x = f . y ) by FUNCT_1:def 3;
ex T1 being DecoratedTree st
( y = T1 & dom T1 = x ) by A4, A5;
hence x is Tree ; :: thesis: verum

end;

then A6: union E is Tree by Th35;
dom T = union E

proof

thus dom T c= union E :: according to XBOOLE_0:def 10 :: thesis: union E c= dom T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom T or x in union E )
assume x in dom T ; :: thesis: x in union E
then consider y being set such that
A7: [x,y] in T by RELAT_1:def 4;
consider X being set such that
A8: [x,y] in X and
A9: X in D by A7, TARSKI:def 4;
consider T1 being DecoratedTree such that
A10: X = T1 and
A11: dom T1 = f . X by A4, A9;
A12: dom T1 in rng f by A4, A9, A11, FUNCT_1:def 3;
A13: x in dom T1 by A8, A10, RELAT_1:def 4;
dom T1 c= union E by A12, ZFMISC_1:74;
hence x in union E by A13; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union E or x in dom T )
assume x in union E ; :: thesis: x in dom T
then consider X being set such that
A14: x in X and
A15: X in E by TARSKI:def 4;
consider y being set such that
A16: y in dom f and
A17: X = f . y by A15, FUNCT_1:def 3;
consider T1 being DecoratedTree such that
A18: y = T1 and
A19: dom T1 = X by A4, A16, A17;
[x,(T1 . x)] in T1 by A14, A19, FUNCT_1:1;
then [x,(T1 . x)] in union D by A4, A16, A18, TARSKI:def 4;
hence x in dom T by RELAT_1:def 4; :: thesis: verum

end;

hence union D is DecoratedTree by A6, Def8; :: thesis: verum