defpred S₁[ 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₁[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₁[x] )

proof

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₁[x] )
thus ( x in A implies S₁[x] ) by A1; :: thesis: ( S₁[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₁[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;

hence ex b₁ being Subset of ((FreeSort X) . s) st
for x being set holds
( x in b₁ iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ; :: thesis: verum