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

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

end;

consider f being Function such that
A4: ( dom f = D & ( for x being object 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;

let x be set ; :: thesis:
assume x in E ; :: thesis:
then consider y being object 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:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in dom T ; :: thesis:
then consider y being object such that
A7: [x,y] in T by XTUPLE_0:def 12;
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, XTUPLE_0:def 12;
dom T1 c= union E by A12, ZFMISC_1:74;
hence x in union E by A13; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union E ; :: thesis:
then consider X being set such that
A14: x in X and
A15: X in E by TARSKI:def 4;
consider y being object 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 XTUPLE_0:def 12; :: thesis:

end;