defpred S_{1}[ object ] means ex a being set st

( a in X . s & $1 = root-tree [a,s] );

set D = DTConMSA X;

consider A being set such that

A1: for x being object holds

( x in A iff ( x in (FreeSort X) . s & S_{1}[x] ) )
from XBOOLE_0:sch 1();

A c= (FreeSort X) . s by A1;

then reconsider A = A as Subset of ((FreeSort X) . s) ;

for x being set holds

( x in A iff S_{1}[x] )
_{1} being Subset of ((FreeSort X) . s) st

for x being set holds

( x in b_{1} iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) ; :: thesis: verum

( a in X . s & $1 = root-tree [a,s] );

set D = DTConMSA X;

consider A being set such that

A1: for x being object holds

( x in A iff ( x in (FreeSort X) . s & S

A c= (FreeSort X) . s by A1;

then reconsider A = A as Subset of ((FreeSort X) . s) ;

for x being set holds

( x in A iff S

proof

hence
ex b
dom (coprod X) = the carrier of S
by PARTFUN1:def 2;

then (coprod X) . s in rng (coprod X) by FUNCT_1:def 3;

then A2: coprod (s,X) in rng (coprod X) by Def3;

A3: Terminals (DTConMSA X) = Union (coprod X) by Th6;

let x be set ; :: thesis: ( x in A iff S_{1}[x] )

thus ( x in A implies S_{1}[x] )
by A1; :: thesis: ( S_{1}[x] implies x in A )

set A = { aa where aa is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & aa = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = aa . {} & the_result_sort_of o1 = s ) ) } ;

assume A4: S_{1}[x]
; :: thesis: x in A

then consider a being set such that

A5: a in X . s and

A6: x = root-tree [a,s] ;

A7: (FreeSort X) . s = FreeSort (X,s) by Def11;

set sa = [a,s];

[a,s] in coprod (s,X) by A5, Def2;

then [a,s] in union (rng (coprod X)) by A2, TARSKI:def 4;

then A8: [a,s] in Terminals (DTConMSA X) by A3, CARD_3:def 4;

then reconsider sa = [a,s] as Symbol of (DTConMSA X) ;

reconsider b = root-tree sa as Element of TS (DTConMSA X) by A8, DTCONSTR:def 1;

b in { aa where aa is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & aa = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = aa . {} & the_result_sort_of o1 = s ) ) } by A5;

hence x in A by A1, A4, A6, A7; :: thesis: verum

end;then (coprod X) . s in rng (coprod X) by FUNCT_1:def 3;

then A2: coprod (s,X) in rng (coprod X) by Def3;

A3: Terminals (DTConMSA X) = Union (coprod X) by Th6;

let x be set ; :: thesis: ( x in A iff S

thus ( x in A implies S

set A = { aa where aa is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & aa = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = aa . {} & the_result_sort_of o1 = s ) ) } ;

assume A4: S

then consider a being set such that

A5: a in X . s and

A6: x = root-tree [a,s] ;

A7: (FreeSort X) . s = FreeSort (X,s) by Def11;

set sa = [a,s];

[a,s] in coprod (s,X) by A5, Def2;

then [a,s] in union (rng (coprod X)) by A2, TARSKI:def 4;

then A8: [a,s] in Terminals (DTConMSA X) by A3, CARD_3:def 4;

then reconsider sa = [a,s] as Symbol of (DTConMSA X) ;

reconsider b = root-tree sa as Element of TS (DTConMSA X) by A8, DTCONSTR:def 1;

b in { aa where aa is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & aa = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = aa . {} & the_result_sort_of o1 = s ) ) } by A5;

hence x in A by A1, A4, A6, A7; :: thesis: verum

for x being set holds

( x in b

( a in X . s & x = root-tree [a,s] ) ) ; :: thesis: verum