set D = DTConOSA X;
set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
A1: Terminals (DTConOSA X) = Union (coprod X) by Th3;
A2: NonTerminals (DTConOSA X) = [: the carrier' of S,{ the carrier of S}:] by Th3;
A3: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:] by MSAFREE:4;
for nt being Symbol of (DTConOSA X) st nt in NonTerminals (DTConOSA X) holds
ex p being FinSequence of TS (DTConOSA X) st nt ==> roots p

let nt be Symbol of (DTConOSA X); :: thesis:
assume nt in NonTerminals (DTConOSA X) ; :: thesis:
then consider o being Element of the carrier' of S, x2 being Element of { the carrier of S} such that
A4: nt = [o,x2] by A2, DOMAIN_1:1;
set O = the_arity_of o;
A5: the carrier of S = x2 by TARSKI:def 1;
defpred S₁[ object , object ] means ex i being Element of S st
( i <= (the_arity_of o) /. S & X in coprod (i,X) );
A6: for a being object st a in Seg (len (the_arity_of o)) holds
ex b being object st S₁[a,b]

let a be object ; :: thesis:
assume a in Seg (len (the_arity_of o)) ; :: thesis:
then A7: a in dom (the_arity_of o) by FINSEQ_1:def 3;
then A8: (the_arity_of o) . a in rng (the_arity_of o) by FUNCT_1:def 3;
A9: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;
then consider x being object such that
A10: x in X . ((the_arity_of o) . a) by A8, XBOOLE_0:def 1;
take y = [x,((the_arity_of o) . a)]; :: thesis:
take (the_arity_of o) /. a ; :: thesis:
y in coprod (((the_arity_of o) . a),X) by A8, A9, A10, MSAFREE:def 2;
hence ( (the_arity_of o) /. a <= (the_arity_of o) /. a & y in coprod (((the_arity_of o) /. a),X) ) by A7, PARTFUN1:def 6; :: thesis:

end;

consider b being Function such that
A11: ( dom b = Seg (len (the_arity_of o)) & ( for a being object st a in Seg (len (the_arity_of o)) holds
S₁[a,b . a] ) ) from CLASSES1:sch 1(A6);
reconsider b = b as FinSequence by A11, FINSEQ_1:def 2;
A12: rng b c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng b ; :: thesis:
then consider c being object such that
A13: c in dom b and
A14: b . c = a by FUNCT_1:def 3;
consider i being Element of S such that
i <= (the_arity_of o) /. c and
A15: a in coprod (i,X) by A11, A13, A14;
dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X) . i in rng (coprod X) by FUNCT_1:def 3;
then coprod (i,X) in rng (coprod X) by MSAFREE:def 3;
then a in union (rng (coprod X)) by A15, TARSKI:def 4;
then a in Union (coprod X) by CARD_3:def 4;
hence a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by XBOOLE_0:def 3; :: thesis:

end;

then reconsider b = b as FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by FINSEQ_1:def 4;
reconsider b = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def 11;
deffunc H₁( object ) -> set = root-tree (b . S);
consider f being Function such that
A16: ( dom f = dom b & ( for x being object st x in dom b holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
reconsider f = f as FinSequence by A11, A16, FINSEQ_1:def 2;
rng f c= TS (DTConOSA X)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being object such that
A17: y in dom f and
A18: f . y = x by FUNCT_1:def 3;
b . y in rng b by A16, A17, FUNCT_1:def 3;
then reconsider a = b . y as Symbol of (DTConOSA X) by A12;
consider i being Element of S such that
i <= (the_arity_of o) /. y and
A19: b . y in coprod (i,X) by A11, A16, A17;
dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X) . i in rng (coprod X) by FUNCT_1:def 3;
then coprod (i,X) in rng (coprod X) by MSAFREE:def 3;
then b . y in union (rng (coprod X)) by A19, TARSKI:def 4;
then A20: a in Terminals (DTConOSA X) by A1, CARD_3:def 4;
x = root-tree (b . y) by A16, A17, A18;
hence x in TS (DTConOSA X) by A20, DTCONSTR:def 1; :: thesis:

end;

then reconsider f = f as FinSequence of TS (DTConOSA X) by FINSEQ_1:def 4;
A21: for x being object st x in dom b holds
(roots f) . x = b . x

let x be object ; :: thesis:
assume A22: x in dom b ; :: thesis:
then reconsider i = x as Nat ;
A23: ex T being DecoratedTree st
( T = f . i & (roots f) . i = T . {} ) by A16, A22, TREES_3:def 18;
f . x = root-tree (b . x) by A16, A22;
hence (roots f) . x = b . x by A23, TREES_4:3; :: thesis:

end;

A24: now :: thesis:

let c be set ; :: thesis:
assume c in dom b ; :: thesis:
then consider i being Element of S such that
A25: i <= (the_arity_of o) /. c and
A26: b . c in coprod (i,X) by A11;
dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X) . i in rng (coprod X) by FUNCT_1:def 3;
then coprod (i,X) in rng (coprod X) by MSAFREE:def 3;
then b . c in union (rng (coprod X)) by A26, TARSKI:def 4;
then b . c in Union (coprod X) by CARD_3:def 4;
hence ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 <= (the_arity_of o) /. c ) by A3, XBOOLE_0:3; :: thesis:
assume b . c in Union (coprod X) ; :: thesis:
thus ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) ) by A25, A26; :: thesis:

end;

len b = len (the_arity_of o) by A11, FINSEQ_1:def 3;
then [nt,b] in OSREL X by A4, A5, A24, Th2;
then A27: nt ==> b by LANG1:def 1;
take f ; :: thesis:
dom (roots f) = dom f by TREES_3:def 18;
hence nt ==> roots f by A27, A16, A21, FUNCT_1:2; :: thesis:

end;

hence ( DTConOSA X is with_terminals & DTConOSA X is with_nonterminals & DTConOSA X is with_useful_nonterminals ) by A1, A2, DTCONSTR:def 3, DTCONSTR:def 4, DTCONSTR:def 5; :: thesis: