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 );
A4: 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;
( x = T1 & dom T1 = dom T1 ) ;
hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

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

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
A6: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
ex T1 being DecoratedTree st
( y = T1 & dom T1 = x ) by A5, A6;
hence x is Tree ; :: thesis: verum

end;

then A7: 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
A8: [x,y] in T by RELAT_1:def 4;
consider X being set such that
A9: ( [x,y] in X & X in D ) by A8, TARSKI:def 4;
consider T1 being DecoratedTree such that
A10: ( X = T1 & dom T1 = f . X ) by A5, A9;
( X = T1 & dom T1 in rng f ) by A5, A9, A10, FUNCT_1:def 5;
then ( x in dom T1 & dom T1 c= union E ) by A9, RELAT_1:def 4, ZFMISC_1:92;
hence x in union E ; :: 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
A11: ( x in X & X in E ) by TARSKI:def 4;
consider y being set such that
A12: ( y in dom f & X = f . y ) by A11, FUNCT_1:def 5;
consider T1 being DecoratedTree such that
A13: ( y = T1 & dom T1 = X ) by A5, A12;
( [x,(T1 . x)] in T1 & T1 = T1 ) by A11, A13, FUNCT_1:8;
then ( [x,(T1 . x)] in union D & T = T ) by A5, A12, A13, TARSKI:def 4;
hence x in dom T by RELAT_1:def 4; :: thesis: verum

end;

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