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 MSAFREE:def 3;
set A = { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) 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 (DTConOSA X) = Union (coprod X)
by Th3;
[x,s] in coprod (s,X)
by A2, MSAFREE:def 2;
then
[x,s] in union (rng (coprod X))
by A1, TARSKI:def 4;
then A4:
[x,s] in Terminals (DTConOSA X)
by A3, CARD_3:def 4;
then reconsider a = [x,s] as Symbol of (DTConOSA X) ;
reconsider b = root-tree a as Element of TS (DTConOSA X) by A4, DTCONSTR:def 1;
b in { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) }
by A2;
hence
not ParsedTerms (X,s) is empty
; verum