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 A1: coprod (s,X) in rng (coprod X) by Def3;

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

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

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

consider x being object such that

A2: x in X . s by XBOOLE_0:def 1;

set a = [x,s];

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

[x,s] in coprod (s,X) by A2, Def2;

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

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

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

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

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

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

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } by A2;

hence not FreeSort (X,s) is empty ; :: thesis: verum

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

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

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

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

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

consider x being object such that

A2: x in X . s by XBOOLE_0:def 1;

set a = [x,s];

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

[x,s] in coprod (s,X) by A2, Def2;

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

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

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

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

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

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

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } by A2;

hence not FreeSort (X,s) is empty ; :: thesis: verum