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

end;

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

end;

then A12: 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
A15: [x,y] in T by RELAT_1:def 4;
consider X being set such that
A16: [x,y] in X and
A17: X in D by A15, TARSKI:def 4;
consider T1 being DecoratedTree such that
A18: X = T1 and
A19: dom T1 = f . X by A7, A17;
A20: dom T1 in rng f by A7, A17, A19, FUNCT_1:def 5;
A21: x in dom T1 by A16, A18, RELAT_1:def 4;
dom T1 c= union E by A20, ZFMISC_1:92;
hence x in union E by A21; :: 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
A24: x in X and
A25: X in E by TARSKI:def 4;
consider y being set such that
A26: y in dom f and
A27: X = f . y by A25, FUNCT_1:def 5;
consider T1 being DecoratedTree such that
A28: y = T1 and
A29: dom T1 = X by A7, A26, A27;
[x,(T1 . x)] in T1 by A24, A29, FUNCT_1:8;
then [x,(T1 . x)] in union D by A7, A26, A28, TARSKI:def 4;
hence x in dom T by RELAT_1:def 4; :: thesis: verum

end;

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