let D be non empty set ; ( ( 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
; union D is DecoratedTree
A3:
for x being set st x in D holds
x is Function
by A1;
reconsider T = union D as Function by A2, A3, Th36;
defpred S1[ 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 S1[x,y]
consider f being Function such that
A7:
( dom f = D & ( for x being set st x in D holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A4);
reconsider E = rng f as non empty set by A7, RELAT_1:65;
A12:
union E is Tree
by A8, Th35;
A13:
dom T = union E
proof
thus
dom T c= union E
XBOOLE_0:def 10 union E c= dom Tproof
let x be
set ;
TARSKI:def 3 ( not x in dom T or x in union E )
assume A14:
x in dom T
;
x in union E
consider y being
set such that A15:
[x,y] in T
by A14, 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;
A22:
dom T1 c= union E
by A20, ZFMISC_1:92;
thus
x in union E
by A21, A22;
verum
end;
let x be
set ;
TARSKI:def 3 ( not x in union E or x in dom T )
assume A23:
x in union E
;
x in dom T
consider X being
set such that A24:
x in X
and A25:
X in E
by A23, 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;
A30:
[x,(T1 . x)] in T1
by A24, A29, FUNCT_1:8;
A31:
[x,(T1 . x)] in union D
by A7, A26, A28, A30, TARSKI:def 4;
thus
x in dom T
by A31, RELAT_1:def 4;
verum
end;
thus
union D is DecoratedTree
by A12, A13, Def8; verum